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 A = E W
sbcie2s.b B = F W
sbcie2s.1 a = A b = B φ ψ
Assertion sbcie2s w = W [˙ E w / a]˙ [˙ F w / b]˙ φ ψ

Proof

Step Hyp Ref Expression
1 sbcie2s.a A = E W
2 sbcie2s.b B = F W
3 sbcie2s.1 a = A b = B φ ψ
4 fvex E w V
5 fvex F w V
6 fveq2 w = W E w = E W
7 6 1 eqtr4di w = W E w = A
8 7 eqeq2d w = W a = E w a = A
9 8 biimpd w = W a = E w a = A
10 fveq2 w = W F w = F W
11 10 2 eqtr4di w = W F w = B
12 11 eqeq2d w = W b = F w b = B
13 12 biimpd w = W b = F w b = B
14 3 a1i w = W a = A b = B φ ψ
15 9 13 14 syl2and w = W a = E w b = F w φ ψ
16 4 5 15 sbc2iedv w = W [˙ E w / a]˙ [˙ F w / b]˙ φ ψ