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

Metamath Proof Explorer

Theorem sbcie2s

Description: A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019) (Revised by SN, 2-Mar-2025)

Ref Expression
Hypotheses sbcie2s.a 
|- A = ( E ` W )
sbcie2s.b 
|- B = ( F ` W )
sbcie2s.1 
|- ( ( a = A /\ b = B ) -> ( ph <-> ps ) )
Assertion sbcie2s 
|- ( w = W -> ( [. ( E ` w ) / a ]. [. ( F ` w ) / b ]. ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 sbcie2s.a 
 |-  A = ( E ` W )
2 sbcie2s.b 
 |-  B = ( F ` W )
3 sbcie2s.1 
 |-  ( ( a = A /\ b = B ) -> ( ph <-> ps ) )
4 fvex 
 |-  ( E ` w ) e. _V
5 fvex 
 |-  ( F ` w ) e. _V
6 fveq2 
 |-  ( w = W -> ( E ` w ) = ( E ` W ) )
7 6 1 eqtr4di 
 |-  ( w = W -> ( E ` w ) = A )
8 7 eqeq2d 
 |-  ( w = W -> ( a = ( E ` w ) <-> a = A ) )
9 8 biimpd 
 |-  ( w = W -> ( a = ( E ` w ) -> a = A ) )
10 fveq2 
 |-  ( w = W -> ( F ` w ) = ( F ` W ) )
11 10 2 eqtr4di 
 |-  ( w = W -> ( F ` w ) = B )
12 11 eqeq2d 
 |-  ( w = W -> ( b = ( F ` w ) <-> b = B ) )
13 12 biimpd 
 |-  ( w = W -> ( b = ( F ` w ) -> b = B ) )
14 3 a1i 
 |-  ( w = W -> ( ( a = A /\ b = B ) -> ( ph <-> ps ) ) )
15 9 13 14 syl2and 
 |-  ( w = W -> ( ( a = ( E ` w ) /\ b = ( F ` w ) ) -> ( ph <-> ps ) ) )
16 4 5 15 sbc2iedv 
 |-  ( w = W -> ( [. ( E ` w ) / a ]. [. ( F ` w ) / b ]. ph <-> ps ) )