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

Metamath Proof Explorer

Theorem sbc2iedv

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008) (Proof shortened by Mario Carneiro, 18-Oct-2016)

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

Proof

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