Metamath Proof Explorer


Theorem zfcndac

Description: Axiom of Choice ax-ac , reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion zfcndac y z w z w w x v u t u w w t u t t y u = v

Proof

Step Hyp Ref Expression
1 axacnd y z w y z w w x x z x z w w x z x x y z = x
2 19.3v y z w w x z w w x
3 2 imbi1i y z w w x x z x z w w x z x x y z = x z w w x x z x z w w x z x x y z = x
4 3 2albii z w y z w w x x z x z w w x z x x y z = x z w z w w x x z x z w w x z x x y z = x
5 4 exbii y z w y z w w x x z x z w w x z x x y z = x y z w z w w x x z x z w w x z x x y z = x
6 1 5 mpbi y z w z w w x x z x z w w x z x x y z = x
7 equequ2 v = x u = v u = x
8 7 bibi2d v = x t u w w t u t t y u = v t u w w t u t t y u = x
9 elequ2 t = x w t w x
10 9 anbi2d t = x u w w t u w w x
11 elequ2 t = x u t u x
12 elequ1 t = x t y x y
13 11 12 anbi12d t = x u t t y u x x y
14 10 13 anbi12d t = x u w w t u t t y u w w x u x x y
15 14 cbvexvw t u w w t u t t y x u w w x u x x y
16 15 bibi1i t u w w t u t t y u = x x u w w x u x x y u = x
17 8 16 bitrdi v = x t u w w t u t t y u = v x u w w x u x x y u = x
18 17 albidv v = x u t u w w t u t t y u = v u x u w w x u x x y u = x
19 elequ1 u = z u w z w
20 19 anbi1d u = z u w w x z w w x
21 elequ1 u = z u x z x
22 21 anbi1d u = z u x x y z x x y
23 20 22 anbi12d u = z u w w x u x x y z w w x z x x y
24 23 exbidv u = z x u w w x u x x y x z w w x z x x y
25 equequ1 u = z u = x z = x
26 24 25 bibi12d u = z x u w w x u x x y u = x x z w w x z x x y z = x
27 26 cbvalvw u x u w w x u x x y u = x z x z w w x z x x y z = x
28 18 27 bitrdi v = x u t u w w t u t t y u = v z x z w w x z x x y z = x
29 28 cbvexvw v u t u w w t u t t y u = v x z x z w w x z x x y z = x
30 29 imbi2i z w w x v u t u w w t u t t y u = v z w w x x z x z w w x z x x y z = x
31 30 2albii z w z w w x v u t u w w t u t t y u = v z w z w w x x z x z w w x z x x y z = x
32 31 exbii y z w z w w x v u t u w w t u t t y u = v y z w z w w x x z x z w w x z x x y z = x
33 6 32 mpbir y z w z w w x v u t u w w t u t t y u = v