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 ( 𝑤 = 𝑊 → ( [ ( 𝐸𝑤 ) / 𝑎 ] [ ( 𝐹𝑤 ) / 𝑏 ] 𝜑𝜓 ) )