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

Proof

Step	Hyp	Ref	Expression
1		sbcie2s.a	⊢ 𝐴 = ( 𝐸 ‘ 𝑊 )
2		sbcie2s.b	⊢ 𝐵 = ( 𝐹 ‘ 𝑊 )
3		sbcie2s.1	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
4		fvex	⊢ ( 𝐸 ‘ 𝑤 ) ∈ V
5		fvex	⊢ ( 𝐹 ‘ 𝑤 ) ∈ V
6		simprl	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → 𝑎 = ( 𝐸 ‘ 𝑤 ) )
7		fveq2	⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑊 ) )
8	7 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = 𝐴 )
9	8	adantr	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝐸 ‘ 𝑤 ) = 𝐴 )
10	6 9	eqtrd	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → 𝑎 = 𝐴 )
11		simprr	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → 𝑏 = ( 𝐹 ‘ 𝑤 ) )
12		fveq2	⊢ ( 𝑤 = 𝑊 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑊 ) )
13	12 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 𝐹 ‘ 𝑤 ) = 𝐵 )
14	13	adantr	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝐹 ‘ 𝑤 ) = 𝐵 )
15	11 14	eqtrd	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → 𝑏 = 𝐵 )
16	10 15 3	syl2anc	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝜑 ↔ 𝜓 ) )
17	16	bicomd	⊢ ( ( 𝑤 = 𝑊 ∧ ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝜓 ↔ 𝜑 ) )
18	17	ex	⊢ ( 𝑤 = 𝑊 → ( ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) → ( 𝜓 ↔ 𝜑 ) ) )
19	4 5 18	sbc2iedv	⊢ ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] [ ( 𝐹 ‘ 𝑤 ) / 𝑏 ] 𝜓 ↔ 𝜑 ) )