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 ⊢ 𝐴 ∈ V
csbie2t.2 ⊢ 𝐵 ∈ V
Assertion csbie2t ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )

Proof

Step Hyp Ref Expression
1 csbie2t.1 ⊢ 𝐴 ∈ V
2 csbie2t.2 ⊢ 𝐵 ∈ V
3 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
4 nfcvd ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → Ⅎ 𝑥 𝐷 )
5 1 a1i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → 𝐴 ∈ V )
6 nfa2 ⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
7 nfv ⊢ Ⅎ 𝑦 𝑥 = 𝐴
8 6 7 nfan ⊢ Ⅎ 𝑦 ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 )
9 nfcvd ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → Ⅎ 𝑦 𝐷 )
10 2 a1i ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ V )
11 2sp ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) )
12 11 impl ⊢ ( ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 )
13 8 9 10 12 csbiedf ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) ∧ 𝑥 = 𝐴 ) → ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )
14 3 4 5 13 csbiedf ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐷 )