HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem aceq0 4702
Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac 4716.
Assertion
Ref Expression
aceq0 |- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)))
Distinct variable group:   x,y,z,w,v,u,t
Proof of Theorem aceq0
StepHypRef Expression
1 aceq1 4701 . 2 |- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.zA.w((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
2 equequ2 1131 . . . . . . . . . 10 |- (v = x -> (u = v <-> u = x))
32bibi2d 616 . . . . . . . . 9 |- (v = x -> ((E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v) <-> (E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = x)))
4 elequ2 1133 . . . . . . . . . . . . 13 |- (t = x -> (w e. t <-> w e. x))
54anbi2d 614 . . . . . . . . . . . 12 |- (t = x -> ((u e. w /\ w e. t) <-> (u e. w /\ w e. x)))
6 elequ2 1133 . . . . . . . . . . . . 13 |- (t = x -> (u e. t <-> u e. x))
7 elequ1 1132 . . . . . . . . . . . . 13 |- (t = x -> (t e. y <-> x e. y))
86, 7anbi12d 626 . . . . . . . . . . . 12 |- (t = x -> ((u e. t /\ t e. y) <-> (u e. x /\ x e. y)))
95, 8anbi12d 626 . . . . . . . . . . 11 |- (t = x -> (((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> ((u e. w /\ w e. x) /\ (u e. x /\ x e. y))))
109cbvexv 1310 . . . . . . . . . 10 |- (E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)))
1110bibi1i 607 . . . . . . . . 9 |- ((E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = x) <-> (E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> u = x))
123, 11syl6bb 534 . . . . . . . 8 |- (v = x -> ((E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v) <-> (E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> u = x)))
1312albidv 1273 . . . . . . 7 |- (v = x -> (A.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v) <-> A.u(E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> u = x)))
14 elequ1 1132 . . . . . . . . . . . 12 |- (u = z -> (u e. w <-> z e. w))
1514anbi1d 615 . . . . . . . . . . 11 |- (u = z -> ((u e. w /\ w e. x) <-> (z e. w /\ w e. x)))
16 elequ1 1132 . . . . . . . . . . . 12 |- (u = z -> (u e. x <-> z e. x))
1716anbi1d 615 . . . . . . . . . . 11 |- (u = z -> ((u e. x /\ x e. y) <-> (z e. x /\ x e. y)))
1815, 17anbi12d 626 . . . . . . . . . 10 |- (u = z -> (((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> ((z e. w /\ w e. x) /\ (z e. x /\ x e. y))))
1918exbidv 1274 . . . . . . . . 9 |- (u = z -> (E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y))))
20 equequ1 1130 . . . . . . . . 9 |- (u = z -> (u = x <-> z = x))
2119, 20bibi12d 627 . . . . . . . 8 |- (u = z -> ((E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> u = x) <-> (E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
2221cbvalv 1309 . . . . . . 7 |- (A.u(E.x((u e. w /\ w e. x) /\ (u e. x /\ x e. y)) <-> u = x) <-> A.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))
2313, 22syl6bb 534 . . . . . 6 |- (v = x -> (A.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v) <-> A.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
2423cbvexv 1310 . . . . 5 |- (E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v) <-> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x))
2524imbi2i 185 . . . 4 |- (((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)) <-> ((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
26252albii 997 . . 3 |- (A.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)) <-> A.zA.w((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
2726exbii 1047 . 2 |- (E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)) <-> E.yA.zA.w((z e. w /\ w e. x) -> E.xA.z(E.x((z e. w /\ w e. x) /\ (z e. x /\ x e. y)) <-> z = x)))
281, 27bitr4 176 1 |- (E.yA.z e. x A.w e. z E!v e. z E.u e. y (z e. u /\ v e. u) <-> E.yA.zA.w((z e. w /\ w e. x) -> E.vA.u(E.t((u e. w /\ w e. t) /\ (u e. t /\ t e. y)) <-> u = v)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  A.wral 1637  E.wrex 1638  E!wreu 1639
This theorem is referenced by:  ac2 4718
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-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-11o 1213  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-cleq 1462  df-clel 1465  df-ral 1641  df-rex 1642  df-reu 1643
Copyright terms: Public domain