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

Metamath Proof Explorer

Theorem sbc2iegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013)

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

Proof

Step Hyp Ref Expression
1 sbc2iegf.1 ⊢ Ⅎ x ψ
2 sbc2iegf.2 ⊢ Ⅎ y ψ
3 sbc2iegf.3 ⊢ Ⅎ x B ∈ W
4 sbc2iegf.4 ⊢ x = A ∧ y = B → φ ↔ ψ
5 simpl ⊢ A ∈ V ∧ B ∈ W → A ∈ V
6 simpl ⊢ B ∈ W ∧ x = A → B ∈ W
7 4 adantll ⊢ B ∈ W ∧ x = A ∧ y = B → φ ↔ ψ
8 nfv ⊢ Ⅎ y B ∈ W ∧ x = A
9 2 a1i ⊢ B ∈ W ∧ x = A → Ⅎ y ψ
10 6 7 8 9 sbciedf ⊢ B ∈ W ∧ x = A → [˙B / y]˙ φ ↔ ψ
11 10 adantll ⊢ A ∈ V ∧ B ∈ W ∧ x = A → [˙B / y]˙ φ ↔ ψ
12 nfv ⊢ Ⅎ x A ∈ V
13 12 3 nfan ⊢ Ⅎ x A ∈ V ∧ B ∈ W
14 1 a1i ⊢ A ∈ V ∧ B ∈ W → Ⅎ x ψ
15 5 11 13 14 sbciedf ⊢ A ∈ V ∧ B ∈ W → [˙A / x]˙ [˙B / y]˙ φ ↔ ψ