Theorem csbeq2gVD 45431

Description: Virtual deduction proof of csbeq2 3857. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbeq2 3857 is csbeq2gVD 45431 without virtual deductions and was automatically derived from csbeq2gVD 45431.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥𝐵 = 𝐶 → [𝐴 / 𝑥] 𝐵 = 𝐶)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
4:2,3:	⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥𝐵 = 𝐶 → ⦋𝐴 / 𝑥 ⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
qed:4:	⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌ 𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
csbeq2gVD	⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Proof of Theorem csbeq2gVD

Step	Hyp	Ref	Expression
1		idn1 45114	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		spsbc 3757	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶))
3	1, 2	e1a 45167	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶)   )
4		sbceqg 4365	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
5	1, 4	e1a 45167	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
6		imbi2 350	. . . 4 ⊢ (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ↔ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)))
7	6	biimpcd 251	. . 3 ⊢ ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) → (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)))
8	3, 5, 7	e11 45228	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
9	8	in1 45111	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559   ∈ wcel 2141  [wsbc 3744  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3745  df-csb 3853  df-vd1 45110

This theorem is referenced by: (None)