Theorem moi 1915

Description: Equality implied by "at most one."

Hypotheses

Ref	Expression
moi.1	|- (x = A -> (ph <-> ps))
moi.2	|- (x = B -> (ph <-> ch))

Assertion

Ref	Expression
moi	|- (((A e. C /\ B e. D) /\ E*xph /\ (ps /\ ch)) -> A = B)

Distinct variable groups:   x,A   x,B   ch,x   ps,x

Proof of Theorem moi

Step	Hyp	Ref	Expression
1		ax-17 968	. . . . 5 |- (y e. A -> A.x y e. A)
2		ax-17 968	. . . . . . . 8 |- (ps -> A.xps)
3		hbs1 1327	. . . . . . . 8 |- ([y / x]ph -> A.x[y / x]ph)
4	2, 3	hban 1006	. . . . . . 7 |- ((ps /\ [y / x]ph) -> A.x(ps /\ [y / x]ph))
5		ax-17 968	. . . . . . 7 |- (A = y -> A.x A = y)
6	4, 5	hbim 1004	. . . . . 6 |- (((ps /\ [y / x]ph) -> A = y) -> A.x((ps /\ [y / x]ph) -> A = y))
7	6	hbal 1002	. . . . 5 |- (A.y((ps /\ [y / x]ph) -> A = y) -> A.xA.y((ps /\ [y / x]ph) -> A = y))
8		moi.1	. . . . . . . 8 |- (x = A -> (ph <-> ps))
9	8	anbi1d 615	. . . . . . 7 |- (x = A -> ((ph /\ [y / x]ph) <-> (ps /\ [y / x]ph)))
10		eqeq1 1473	. . . . . . 7 |- (x = A -> (x = y <-> A = y))
11	9, 10	imbi12d 624	. . . . . 6 |- (x = A -> (((ph /\ [y / x]ph) -> x = y) <-> ((ps /\ [y / x]ph) -> A = y)))
12	11	albidv 1273	. . . . 5 |- (x = A -> (A.y((ph /\ [y / x]ph) -> x = y) <-> A.y((ps /\ [y / x]ph) -> A = y)))
13	1, 7, 12	cla4gf 1851	. . . 4 |- (A e. C -> (A.xA.y((ph /\ [y / x]ph) -> x = y) -> A.y((ps /\ [y / x]ph) -> A = y)))
14		visset 1804	. . . . . . . . 9 |- y e. V
15	14	eqvinc 1874	. . . . . . . 8 |- (y = B <-> E.x(x = y /\ x = B))
16		ax-17 968	. . . . . . . . . 10 |- (ch -> A.xch)
17	3, 16	hbbi 1007	. . . . . . . . 9 |- (([y / x]ph <-> ch) -> A.x([y / x]ph <-> ch))
18		sbequ12 1177	. . . . . . . . . . 11 |- (x = y -> (ph <-> [y / x]ph))
19	18	bicomd 519	. . . . . . . . . 10 |- (x = y -> ([y / x]ph <-> ph))
20		moi.2	. . . . . . . . . 10 |- (x = B -> (ph <-> ch))
21	19, 20	sylan9bb 538	. . . . . . . . 9 |- ((x = y /\ x = B) -> ([y / x]ph <-> ch))
22	17, 21	19.23ai 1060	. . . . . . . 8 |- (E.x(x = y /\ x = B) -> ([y / x]ph <-> ch))
23	15, 22	sylbi 199	. . . . . . 7 |- (y = B -> ([y / x]ph <-> ch))
24	23	anbi2d 614	. . . . . 6 |- (y = B -> ((ps /\ [y / x]ph) <-> (ps /\ ch)))
25		eqeq2 1476	. . . . . 6 |- (y = B -> (A = y <-> A = B))
26	24, 25	imbi12d 624	. . . . 5 |- (y = B -> (((ps /\ [y / x]ph) -> A = y) <-> ((ps /\ ch) -> A = B)))
27	26	cla4gv 1853	. . . 4 |- (B e. D -> (A.y((ps /\ [y / x]ph) -> A = y) -> ((ps /\ ch) -> A = B)))
28	13, 27	sylan9 468	. . 3 |- ((A e. C /\ B e. D) -> (A.xA.y((ph /\ [y / x]ph) -> x = y) -> ((ps /\ ch) -> A = B)))
29	3, 18	mo4f 1395	. . 3 |- (E*xph <-> A.xA.y((ph /\ [y / x]ph) -> x = y))
30	28, 29	syl5ib 206	. 2 |- ((A e. C /\ B e. D) -> (E*xph -> ((ps /\ ch) -> A = B)))
31	30	3imp 825	1 |- (((A e. C /\ B e. D) /\ E*xph /\ (ps /\ ch)) -> A = B)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 773  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  [wsbc 1166  E*wmo 1374

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain