Metamath Proof Explorer

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 ⊢ 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 simprl ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → a = E ⁡ w
7 fveq2 ⊢ w = W → E ⁡ w = E ⁡ W
8 7 1 eqtr4di ⊢ w = W → E ⁡ w = A
9 8 adantr ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → E ⁡ w = A
10 6 9 eqtrd ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → a = A
11 simprr ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → b = F ⁡ w
12 fveq2 ⊢ w = W → F ⁡ w = F ⁡ W
13 12 2 eqtr4di ⊢ w = W → F ⁡ w = B
14 13 adantr ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → F ⁡ w = B
15 11 14 eqtrd ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → b = B
16 10 15 3 syl2anc ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → φ ↔ ψ
17 16 bicomd ⊢ w = W ∧ a = E ⁡ w ∧ b = F ⁡ w → ψ ↔ φ
18 17 ex ⊢ w = W → a = E ⁡ w ∧ b = F ⁡ w → ψ ↔ φ
19 4 5 18 sbc2iedv ⊢ w = W → [˙ E ⁡ w / a]˙ [˙ F ⁡ w / b]˙ ψ ↔ φ