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 ⊢ 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]˙ φ ↔ ψ