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

Metamath Proof Explorer

Theorem sbcie3s

Description: A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 15-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 sbcie3s.a 
 |-  A = ( E ` W )
2 sbcie3s.b 
 |-  B = ( F ` W )
3 sbcie3s.c 
 |-  C = ( G ` W )
4 sbcie3s.1 
 |-  ( ( a = A /\ b = B /\ c = C ) -> ( ph <-> ps ) )
5 fvexd 
 |-  ( w = W -> ( E ` w ) e. _V )
6 fvexd 
 |-  ( ( w = W /\ a = ( E ` w ) ) -> ( F ` w ) e. _V )
7 fvexd 
 |-  ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) -> ( G ` w ) e. _V )
8 simpllr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> a = ( E ` w ) )
9 fveq2 
 |-  ( w = W -> ( E ` w ) = ( E ` W ) )
10 9 ad3antrrr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> ( E ` w ) = ( E ` W ) )
11 8 10 eqtrd 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> a = ( E ` W ) )
12 11 1 eqtr4di 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> a = A )
13 simplr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> b = ( F ` w ) )
14 fveq2 
 |-  ( w = W -> ( F ` w ) = ( F ` W ) )
15 14 ad3antrrr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> ( F ` w ) = ( F ` W ) )
16 13 15 eqtrd 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> b = ( F ` W ) )
17 16 2 eqtr4di 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> b = B )
18 simpr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> c = ( G ` w ) )
19 fveq2 
 |-  ( w = W -> ( G ` w ) = ( G ` W ) )
20 19 ad3antrrr 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> ( G ` w ) = ( G ` W ) )
21 18 20 eqtrd 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> c = ( G ` W ) )
22 21 3 eqtr4di 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> c = C )
23 12 17 22 4 syl3anc 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> ( ph <-> ps ) )
24 23 bicomd 
 |-  ( ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) /\ c = ( G ` w ) ) -> ( ps <-> ph ) )
25 7 24 sbcied 
 |-  ( ( ( w = W /\ a = ( E ` w ) ) /\ b = ( F ` w ) ) -> ( [. ( G ` w ) / c ]. ps <-> ph ) )
26 6 25 sbcied 
 |-  ( ( w = W /\ a = ( E ` w ) ) -> ( [. ( F ` w ) / b ]. [. ( G ` w ) / c ]. ps <-> ph ) )
27 5 26 sbcied 
 |-  ( w = W -> ( [. ( E ` w ) / a ]. [. ( F ` w ) / b ]. [. ( G ` w ) / c ]. ps <-> ph ) )