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

Metamath Proof Explorer

Theorem csbie2

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007)

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

Proof

Step Hyp Ref Expression
1 csbie2t.1 ⊢ A ∈ V
2 csbie2t.2 ⊢ B ∈ V
3 csbie2.3 ⊢ x = A ∧ y = B → C = D
4 3 gen2 ⊢ ∀ x ∀ y x = A ∧ y = B → C = D
5 1 2 csbie2t ⊢ ∀ x ∀ y x = A ∧ y = B → C = D → ⦋ A / x⦌ ⦋ B / y⦌ C = D
6 4 5 ax-mp ⊢ ⦋ A / x⦌ ⦋ B / y⦌ C = D