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	⊢ 𝐴 = ( 𝐸 ‘ 𝑊 )
	sbcies.1	⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	sbcies	⊢ ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] 𝜓 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcies.a	⊢ 𝐴 = ( 𝐸 ‘ 𝑊 )
2		sbcies.1	⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		fvexd	⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) ∈ V )
4		simpr	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → 𝑎 = ( 𝐸 ‘ 𝑤 ) )
5		fveq2	⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑊 ) )
6	1 5	eqtr4id	⊢ ( 𝑤 = 𝑊 → 𝐴 = ( 𝐸 ‘ 𝑤 ) )
7	6	adantr	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → 𝐴 = ( 𝐸 ‘ 𝑤 ) )
8	4 7	eqtr4d	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → 𝑎 = 𝐴 )
9	8 2	syl	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → ( 𝜑 ↔ 𝜓 ) )
10	9	bicomd	⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → ( 𝜓 ↔ 𝜑 ) )
11	3 10	sbcied	⊢ ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] 𝜓 ↔ 𝜑 ) )