domex.html was here:

Here is a file domex.html, that shows as an example how you
can prove some ALL(a):[a e dom => f(a) e cod], without
having it as an axiom:
https://groups.google.com/g/sci.math/c/on3M3w_8t6Q/m/sWOSREt_BQAJ

So you only need f(x)=y & g(x)=y, and you will
get some dom and cod, and then you will get f ~ g.

LoL

Mostowski Collapse schrieb am Donnerstag, 21. April 2022 um 21:16:38 UTC+2:
> You can also prove ALL(a):[a e s => f(a) e s] and
> ALL(a):[a e s => f(a) e s], and elimate it from your
> theorem. I already posted a file domex.html a
>
> few days ago here on sci.math. Now do the same
> with f(x)=y & g(x)=y, and you will arrive at the following:
>
> f ~ g <=> EXIST(x):EXIST(y):[f(x)=y & g(x)=y]
>
> Which basically says two functions are equal if
> the intersect, which of course nonsense,
>
> not equality as we understand it, therefore your
> ad hoc axiom is nonsense.
> Dan Christensen schrieb am Donnerstag, 21. April 2022 um 18:37:36 UTC+2:
> > On Thursday, April 21, 2022 at 11:50:29 AM UTC-4, Ben wrote:
> > > Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> > >
> > > > On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
> > > >> Dan Christensen writes:
> > > >>
> > > >
> > > > See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm
> >
> > > Please remove my name from your website -- both in file names and in any
> > > pages where you might have used it.
> > >
> > > Also what you prove is not my theorem.
> > It's an original theorem AFAIK. You recently posted it here originally.
> > > Why would you dishonestly
> > > pretend that it is?
> >
> > > What you show is your attempt to make
> > > ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > look less silly.
> > >
> > More readable and transparent.
> > > If you asked a student (your target audience I think) to write, in DC
> > > Proof, that the equality of all pairs of two things was a consequence of
> > > some predicate, they would write (I hope)
> > >
> > > ALL(x):ALL(y):[P(x,y) => x=y]
> > >
> > That should be:
> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & EXIST(a):a in dom & EXIST(a):a in cod
> > & ALL(a):[a in dom => f1(a) in cod]
> > & ALL(a):[a in dom => f2(a) in cod]
> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> > > And I hope they would question (indeed reject) an axiom that allowed
> > > that predicate to be x(0)=0 & y(0)=0.
> > >
> > Don't know what you are getting at, but they should be able to easily prove:
> >
> > ALL(x0):[EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> > => EXIST(s):ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> >
> > For a more opaque presentation, they could, as you did, leave out "ALL(a):[a in s => f(a) in s] & ALL(a):[a in s => g(a) in s]" in the final conclusion. It might cost them a mark or 2 for poor style. For the record, following is the full text of Ben's Singleton Theorem. (Sorry about the length.)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> > THEOREM
> >
> > ALL(x0):[EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> > => EXIST(s):ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> >
> > PROOF
> >
> > Functional Equality Axiom (1 variable)
> > 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & EXIST(a):a in dom & EXIST(a):a in cod
> > & ALL(a):[a in dom => f1(a) in cod]
> > & ALL(a):[a in dom => f2(a) in cod]
> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> > Fn Equality
> >
> >
> > Suppose...
> >
> > 2 EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> > Premise
> >
> > 3 Set(s) & ALL(a):[a in s <=> a=x0]
> > E Spec, 2
> >
> >
> > Define: s s = {x0}
> >
> > 4 Set(s)
> > Split, 3
> >
> > 5 ALL(a):[a in s <=> a=x0]
> > Split, 3
> >
> > Apply Functional Equality
> > 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> > & EXIST(a):a in s & EXIST(a):a in cod
> > & ALL(a):[a in s => f1(a) in cod]
> > & ALL(a):[a in s => f2(a) in cod]
> > => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> > U Spec, 1
> >
> > 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f1(a) in s]
> > & ALL(a):[a in s => f2(a) in s]
> > => [f1=f2 <=> ALL(a):[a in s => f1(a)=f2(a)]]]
> > U Spec, 6
> >
> > 8 x0 in s <=> x0=x0
> > U Spec, 5
> >
> > 9 [x0 in s => x0=x0] & [x0=x0 => x0 in s]
> > Iff-And, 8
> >
> > 10 x0 in s => x0=x0
> > Split, 9
> >
> > 11 x0=x0 => x0 in s
> > Split, 9
> >
> > 12 x0=x0
> > Reflex
> >
> > As Required:
> >
> > 13 x0 in s
> > Detach, 11, 12
> >
> > As Required:
> >
> > 14 EXIST(a):a in s
> > E Gen, 13
> >
> >
> > Prove: ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]
> > Suppose...
> >
> > 15 f(x0)=x0 & g(x0)=x0
> > Premise
> >
> >
> > Prove: ALL(a):[a in s => f(a) in s]
> >
> > Suppose...
> >
> > 16 z in s
> > Premise
> >
> > 17 z in s <=> z=x0
> > U Spec, 5
> >
> > 18 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 17
> >
> > 19 z in s => z=x0
> > Split, 18
> >
> > 20 z=x0 => z in s
> > Split, 18
> >
> > 21 z=x0
> > Detach, 19, 16
> >
> > 22 x0 in s
> > Substitute, 21, 16
> >
> > 23 f(x0)=x0
> > Split, 15
> >
> > 24 g(x0)=x0
> > Split, 15
> >
> > 25 f(x0) in s
> > Substitute, 23, 22
> >
> > 26 f(z) in s
> > Substitute, 21, 25
> >
> > As Required:
> >
> > 27 ALL(a):[a in s => f(a) in s]
> > Conclusion, 16
> >
> >
> > Prove: ALL(a):[a in s => g(a) in s]
> >
> > Suppose...
> >
> > 28 z in s
> > Premise
> >
> > 29 z in s <=> z=x0
> > U Spec, 5
> >
> > 30 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 29
> >
> > 31 z in s => z=x0
> > Split, 30
> >
> > 32 z=x0 => z in s
> > Split, 30
> >
> > 33 z=x0
> > Detach, 31, 28
> >
> > 34 x0 in s
> > Substitute, 33, 28
> >
> > 35 f(x0)=x0
> > Split, 15
> >
> > 36 g(x0)=x0
> > Split, 15
> >
> > 37 g(x0) in s
> > Substitute, 36, 34
> >
> > 38 g(z) in s
> > Substitute, 33, 37
> >
> > As Required:
> >
> > 39 ALL(a):[a in s => g(a) in s]
> > Conclusion, 28
> >
> > 40 ALL(f2):[Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => f2(a) in s]
> > => [f=f2 <=> ALL(a):[a in s => f(a)=f2(a)]]]
> > U Spec, 7
> >
> > 41 Set(s) & Set(s)
> > & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > => [f=g <=> ALL(a):[a in s => f(a)=g(a)]]
> > U Spec, 40
> >
> > 42 Set(s) & Set(s)
> > Join, 4, 4
> > 43 Set(s) & Set(s) & EXIST(a):a in s
> > Join, 42, 14
> >
> > 44 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > Join, 43, 14
> >
> > 45 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > Join, 44, 27
> >
> > 46 Set(s) & Set(s) & EXIST(a):a in s & EXIST(a):a in s
> > & ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > Join, 45, 39
> >
> > 47 f=g <=> ALL(a):[a in s => f(a)=g(a)]
> > Detach, 41, 46
> >
> > 48 [f=g => ALL(a):[a in s => f(a)=g(a)]]
> > & [ALL(a):[a in s => f(a)=g(a)] => f=g]
> > Iff-And, 47
> >
> > 49 f=g => ALL(a):[a in s => f(a)=g(a)]
> > Split, 48
> >
> > Sufficient: For f=g
> >
> > 50 ALL(a):[a in s => f(a)=g(a)] => f=g
> > Split, 48
> >
> >
> > Prove: ALL(a):[a in s => f(a)=g(a)]
> >
> > Suppose...
> >
> > 51 z in s
> > Premise
> >
> > 52 z in s <=> z=x0
> > U Spec, 5
> >
> > 53 [z in s => z=x0] & [z=x0 => z in s]
> > Iff-And, 52
> >
> > 54 z in s => z=x0
> > Split, 53
> >
> > 55 z=x0 => z in s
> > Split, 53
> >
> > 56 z=x0
> > Detach, 54, 51
> >
> > 57 f(x0)=x0
> > Split, 15
> >
> > 58 g(x0)=x0
> > Split, 15
> >
> > 59 z=g(x0)
> > Substitute, 58, 56
> >
> > 60 x0=g(x0)
> > Substitute, 56, 59
> >
> > 61 f(x0)=g(x0)
> > Substitute, 57, 60
> >
> > 62 f(z)=g(z)
> > Substitute, 56, 61
> > As Required:
> >
> > 63 ALL(a):[a in s => f(a)=g(a)]
> > Conclusion, 51
> >
> > 64 f=g
> > Detach, 50, 63
> > 65 ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > Join, 27, 39
> > 66 ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g
> > Join, 65, 64
> > As Required:
> >
> > 67 ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]
> > Conclusion, 15
> > As Required:
> >
> > 68 ALL(x0):[EXIST(x):[Set(x) & ALL(a):[a in x <=> a=x0]]
> > => EXIST(s):ALL(f):ALL(g):[f(x0)=x0 & g(x0)=x0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]]
> > Conclusion, 2