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

Metamath Proof Explorer

Theorem csbie2t

Description: Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 ). (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses csbie2t.1 ⊢ A ∈ V
csbie2t.2 ⊢ B ∈ V
Assertion csbie2t ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → ⦋ A / x⦌ ⦋ B / y⦌ C = D

Proof

Step Hyp Ref Expression
1 csbie2t.1 ⊢ A ∈ V
2 csbie2t.2 ⊢ B ∈ V
3 nfa1 ⊢ Ⅎ x ∀ x ∀ y x = A ∧ y = B → C = D
4 nfcvd ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → Ⅎ _ x D
5 1 a1i ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → A ∈ V
6 nfa2 ⊢ Ⅎ y ∀ x ∀ y x = A ∧ y = B → C = D
7 nfv ⊢ Ⅎ y x = A
8 6 7 nfan ⊢ Ⅎ y ∀ x ∀ y x = A ∧ y = B → C = D ∧ x = A
9 nfcvd ⊢ ∀ x ∀ y x = A ∧ y = B → C = D ∧ x = A → Ⅎ _ y D
10 2 a1i ⊢ ∀ x ∀ y x = A ∧ y = B → C = D ∧ x = A → B ∈ V
11 2sp ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → x = A ∧ y = B → C = D
12 11 impl ⊢ ∀ x ∀ y x = A ∧ y = B → C = D ∧ x = A ∧ y = B → C = D
13 8 9 10 12 csbiedf ⊢ ∀ x ∀ y x = A ∧ y = B → C = D ∧ x = A → ⦋ B / y⦌ C = D
14 3 4 5 13 csbiedf ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → ⦋ A / x⦌ ⦋ B / y⦌ C = D