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

Metamath Proof Explorer

Theorem sbcie2s

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

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 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑊 ) )
7 6 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = 𝐴 )
8 7 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ↔ 𝑎 = 𝐴 ) )
9 8 biimpd ⊢ ( 𝑤 = 𝑊 → ( 𝑎 = ( 𝐸 ‘ 𝑤 ) → 𝑎 = 𝐴 ) )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑊 ) )
11 10 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 𝐹 ‘ 𝑤 ) = 𝐵 )
12 11 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑏 = ( 𝐹 ‘ 𝑤 ) ↔ 𝑏 = 𝐵 ) )
13 12 biimpd ⊢ ( 𝑤 = 𝑊 → ( 𝑏 = ( 𝐹 ‘ 𝑤 ) → 𝑏 = 𝐵 ) )
14 3 a1i ⊢ ( 𝑤 = 𝑊 → ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) ) )
15 9 13 14 syl2and ⊢ ( 𝑤 = 𝑊 → ( ( 𝑎 = ( 𝐸 ‘ 𝑤 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) → ( 𝜑 ↔ 𝜓 ) ) )
16 4 5 15 sbc2iedv ⊢ ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] [ ( 𝐹 ‘ 𝑤 ) / 𝑏 ] 𝜑 ↔ 𝜓 ) )