Theorem sbcies

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

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

Proof

Step	Hyp	Ref	Expression
1		sbcies.a	|- A = ( E ` W )
2		sbcies.1	|- ( a = A -> ( ph <-> ps ) )
3		fvexd	|- ( w = W -> ( E ` w ) e. _V )
4		simpr	|- ( ( w = W /\ a = ( E ` w ) ) -> a = ( E ` w ) )
5		fveq2	|- ( w = W -> ( E ` w ) = ( E ` W ) )
6	1 5	eqtr4id	|- ( w = W -> A = ( E ` w ) )
7	6	adantr	|- ( ( w = W /\ a = ( E ` w ) ) -> A = ( E ` w ) )
8	4 7	eqtr4d	|- ( ( w = W /\ a = ( E ` w ) ) -> a = A )
9	8 2	syl	|- ( ( w = W /\ a = ( E ` w ) ) -> ( ph <-> ps ) )
10	9	bicomd	|- ( ( w = W /\ a = ( E ` w ) ) -> ( ps <-> ph ) )
11	3 10	sbcied	|- ( w = W -> ( [. ( E ` w ) / a ]. ps <-> ph ) )