This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj941

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj941.1 
|- G = ( f u. { <. n , C >. } )
Assertion bnj941 
|- ( C e. _V -> ( ( p = suc n /\ f Fn n ) -> G Fn p ) )

Proof

Step Hyp Ref Expression
1 bnj941.1 
 |-  G = ( f u. { <. n , C >. } )
2 opeq2 
 |-  ( C = if ( C e. _V , C , (/) ) -> <. n , C >. = <. n , if ( C e. _V , C , (/) ) >. )
3 2 sneqd 
 |-  ( C = if ( C e. _V , C , (/) ) -> { <. n , C >. } = { <. n , if ( C e. _V , C , (/) ) >. } )
4 3 uneq2d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( f u. { <. n , C >. } ) = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) )
5 1 4 eqtrid 
 |-  ( C = if ( C e. _V , C , (/) ) -> G = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) )
6 5 fneq1d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( G Fn p <-> ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) Fn p ) )
7 6 imbi2d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( ( ( p = suc n /\ f Fn n ) -> G Fn p ) <-> ( ( p = suc n /\ f Fn n ) -> ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) Fn p ) ) )
8 eqid 
 |-  ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) = ( f u. { <. n , if ( C e. _V , C , (/) ) >. } )
9 0ex 
 |-  (/) e. _V
10 9 elimel 
 |-  if ( C e. _V , C , (/) ) e. _V
11 8 10 bnj927 
 |-  ( ( p = suc n /\ f Fn n ) -> ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) Fn p )
12 7 11 dedth 
 |-  ( C e. _V -> ( ( p = suc n /\ f Fn n ) -> G Fn p ) )