Theorem sbcie2s

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

	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 ]. ps <-> ph ) )

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		simprl	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> a = ( E ` w ) )
7		fveq2	|- ( w = W -> ( E ` w ) = ( E ` W ) )
8	7 1	eqtr4di	|- ( w = W -> ( E ` w ) = A )
9	8	adantr	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> ( E ` w ) = A )
10	6 9	eqtrd	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> a = A )
11		simprr	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> b = ( F ` w ) )
12		fveq2	|- ( w = W -> ( F ` w ) = ( F ` W ) )
13	12 2	eqtr4di	|- ( w = W -> ( F ` w ) = B )
14	13	adantr	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> ( F ` w ) = B )
15	11 14	eqtrd	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> b = B )
16	10 15 3	syl2anc	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> ( ph <-> ps ) )
17	16	bicomd	|- ( ( w = W /\ ( a = ( E ` w ) /\ b = ( F ` w ) ) ) -> ( ps <-> ph ) )
18	17	ex	|- ( w = W -> ( ( a = ( E ` w ) /\ b = ( F ` w ) ) -> ( ps <-> ph ) ) )
19	4 5 18	sbc2iedv	|- ( w = W -> ( [. ( E ` w ) / a ]. [. ( F ` w ) / b ]. ps <-> ph ) )