Theorem 2mo2

Description: Two ways of expressing "there exists at most one ordered pair <. x , y >. such that ph ( x , y ) holds. Note that this is not equivalent to E* x E* y ph . See also 2mo . This is the analogue of 2eu4 for existential uniqueness. (Contributed by Wolf Lammen, 26-Oct-2019) Reduce dependencies on axioms. (Revised by Wolf Lammen, 3-Jan-2023)

	Ref	Expression
Assertion	2mo2	|- ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	|- ( E. z E. w ( A. x ( E. y ph -> x = z ) /\ A. y ( E. x ph -> y = w ) ) <-> ( E. z A. x ( E. y ph -> x = z ) /\ E. w A. y ( E. x ph -> y = w ) ) )
2		jcab	|- ( ( ph -> ( x = z /\ y = w ) ) <-> ( ( ph -> x = z ) /\ ( ph -> y = w ) ) )
3	2	2albii	|- ( A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y ( ( ph -> x = z ) /\ ( ph -> y = w ) ) )
4		19.26-2	|- ( A. x A. y ( ( ph -> x = z ) /\ ( ph -> y = w ) ) <-> ( A. x A. y ( ph -> x = z ) /\ A. x A. y ( ph -> y = w ) ) )
5		19.23v	|- ( A. y ( ph -> x = z ) <-> ( E. y ph -> x = z ) )
6	5	albii	|- ( A. x A. y ( ph -> x = z ) <-> A. x ( E. y ph -> x = z ) )
7		alcom	|- ( A. x A. y ( ph -> y = w ) <-> A. y A. x ( ph -> y = w ) )
8		19.23v	|- ( A. x ( ph -> y = w ) <-> ( E. x ph -> y = w ) )
9	8	albii	|- ( A. y A. x ( ph -> y = w ) <-> A. y ( E. x ph -> y = w ) )
10	7 9	bitri	|- ( A. x A. y ( ph -> y = w ) <-> A. y ( E. x ph -> y = w ) )
11	6 10	anbi12i	|- ( ( A. x A. y ( ph -> x = z ) /\ A. x A. y ( ph -> y = w ) ) <-> ( A. x ( E. y ph -> x = z ) /\ A. y ( E. x ph -> y = w ) ) )
12	3 4 11	3bitri	|- ( A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> ( A. x ( E. y ph -> x = z ) /\ A. y ( E. x ph -> y = w ) ) )
13	12	2exbii	|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> E. z E. w ( A. x ( E. y ph -> x = z ) /\ A. y ( E. x ph -> y = w ) ) )
14		df-mo	|- ( E* x E. y ph <-> E. z A. x ( E. y ph -> x = z ) )
15		df-mo	|- ( E* y E. x ph <-> E. w A. y ( E. x ph -> y = w ) )
16	14 15	anbi12i	|- ( ( E* x E. y ph /\ E* y E. x ph ) <-> ( E. z A. x ( E. y ph -> x = z ) /\ E. w A. y ( E. x ph -> y = w ) ) )
17	1 13 16	3bitr4ri	|- ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )