Metamath Proof Explorer

Theorem onfrALTlem4

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem4 
|- ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 sbcan 
 |-  ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( [. y / x ]. x e. a /\ [. y / x ]. ( a i^i x ) = (/) ) )
2 sbcel1v 
 |-  ( [. y / x ]. x e. a <-> y e. a )
3 vex 
 |-  y e. _V
4 sbceqg 
 |-  ( y e. _V -> ( [. y / x ]. ( a i^i x ) = (/) <-> [_ y / x ]_ ( a i^i x ) = [_ y / x ]_ (/) ) )
5 3 4 ax-mp 
 |-  ( [. y / x ]. ( a i^i x ) = (/) <-> [_ y / x ]_ ( a i^i x ) = [_ y / x ]_ (/) )
6 csbin 
 |-  [_ y / x ]_ ( a i^i x ) = ( [_ y / x ]_ a i^i [_ y / x ]_ x )
7 csbconstg 
 |-  ( y e. _V -> [_ y / x ]_ a = a )
8 3 7 ax-mp 
 |-  [_ y / x ]_ a = a
9 csbvarg 
 |-  ( y e. _V -> [_ y / x ]_ x = y )
10 3 9 ax-mp 
 |-  [_ y / x ]_ x = y
11 8 10 ineq12i 
 |-  ( [_ y / x ]_ a i^i [_ y / x ]_ x ) = ( a i^i y )
12 6 11 eqtri 
 |-  [_ y / x ]_ ( a i^i x ) = ( a i^i y )
13 csb0 
 |-  [_ y / x ]_ (/) = (/)
14 12 13 eqeq12i 
 |-  ( [_ y / x ]_ ( a i^i x ) = [_ y / x ]_ (/) <-> ( a i^i y ) = (/) )
15 5 14 bitri 
 |-  ( [. y / x ]. ( a i^i x ) = (/) <-> ( a i^i y ) = (/) )
16 2 15 anbi12i 
 |-  ( ( [. y / x ]. x e. a /\ [. y / x ]. ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
17 1 16 bitri 
 |-  ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )