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

Metamath Proof Explorer

Theorem sbc2ie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008) (Revised by Mario Carneiro, 19-Dec-2013) (Proof shortened by GG, 12-Oct-2024)

Ref Expression
Hypotheses sbc2ie.1 ⊢ A ∈ V
sbc2ie.2 ⊢ B ∈ V
sbc2ie.3 ⊢ x = A ∧ y = B → φ ↔ ψ
Assertion sbc2ie ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbc2ie.1 ⊢ A ∈ V
2 sbc2ie.2 ⊢ B ∈ V
3 sbc2ie.3 ⊢ x = A ∧ y = B → φ ↔ ψ
4 2 a1i ⊢ x = A → B ∈ V
5 4 3 sbcied ⊢ x = A → [˙B / y]˙ φ ↔ ψ
6 1 5 sbcie ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ ψ