Metamath Proof Explorer

Theorem zfac

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac . (New usage is discouraged.) (Contributed by NM, 14-Aug-2003)

Ref Expression
Assertion zfac 
|- E. x A. y A. z ( ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )

Proof

Step Hyp Ref Expression
1 ax-ac 
 |-  E. x A. y A. z ( ( y e. z /\ z e. w ) -> E. v A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) )
2 equequ2 
 |-  ( v = w -> ( u = v <-> u = w ) )
3 2 bibi2d 
 |-  ( v = w -> ( ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) <-> ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = w ) ) )
4 elequ2 
 |-  ( t = w -> ( z e. t <-> z e. w ) )
5 4 anbi2d 
 |-  ( t = w -> ( ( u e. z /\ z e. t ) <-> ( u e. z /\ z e. w ) ) )
6 elequ2 
 |-  ( t = w -> ( u e. t <-> u e. w ) )
7 elequ1 
 |-  ( t = w -> ( t e. x <-> w e. x ) )
8 6 7 anbi12d 
 |-  ( t = w -> ( ( u e. t /\ t e. x ) <-> ( u e. w /\ w e. x ) ) )
9 5 8 anbi12d 
 |-  ( t = w -> ( ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) ) )
10 9 cbvexvw 
 |-  ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) )
11 10 bibi1i 
 |-  ( ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = w ) <-> ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> u = w ) )
12 3 11 bitrdi 
 |-  ( v = w -> ( ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) <-> ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> u = w ) ) )
13 12 albidv 
 |-  ( v = w -> ( A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) <-> A. u ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> u = w ) ) )
14 elequ1 
 |-  ( u = y -> ( u e. z <-> y e. z ) )
15 14 anbi1d 
 |-  ( u = y -> ( ( u e. z /\ z e. w ) <-> ( y e. z /\ z e. w ) ) )
16 elequ1 
 |-  ( u = y -> ( u e. w <-> y e. w ) )
17 16 anbi1d 
 |-  ( u = y -> ( ( u e. w /\ w e. x ) <-> ( y e. w /\ w e. x ) ) )
18 15 17 anbi12d 
 |-  ( u = y -> ( ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) ) )
19 18 exbidv 
 |-  ( u = y -> ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) ) )
20 equequ1 
 |-  ( u = y -> ( u = w <-> y = w ) )
21 19 20 bibi12d 
 |-  ( u = y -> ( ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> u = w ) <-> ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
22 21 cbvalvw 
 |-  ( A. u ( E. w ( ( u e. z /\ z e. w ) /\ ( u e. w /\ w e. x ) ) <-> u = w ) <-> A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
23 13 22 bitrdi 
 |-  ( v = w -> ( A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) <-> A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
24 23 cbvexvw 
 |-  ( E. v A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) <-> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
25 24 imbi2i 
 |-  ( ( ( y e. z /\ z e. w ) -> E. v A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) ) <-> ( ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
26 25 2albii 
 |-  ( A. y A. z ( ( y e. z /\ z e. w ) -> E. v A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) ) <-> A. y A. z ( ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
27 26 exbii 
 |-  ( E. x A. y A. z ( ( y e. z /\ z e. w ) -> E. v A. u ( E. t ( ( u e. z /\ z e. t ) /\ ( u e. t /\ t e. x ) ) <-> u = v ) ) <-> E. x A. y A. z ( ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
28 1 27 mpbi 
 |-  E. x A. y A. z ( ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )