Theorem csbeq2gVD 39619

Description: Virtual deduction proof of csbeq2gOLD 39259. 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. csbeq2gOLD 39259 is csbeq2gVD 39619 without virtual deductions and was automatically derived from csbeq2gVD 39619.

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 39284	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		spsbc 3581	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶))
3	1, 2	e1a 39346	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶)   )
4		sbceqg 4119	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
5	1, 4	e1a 39346	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
6		imbi2 337	. . . 4 ⊢ (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) ↔ (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)))
7	6	biimpcd 239	. . 3 ⊢ ((∀𝑥 𝐵 = 𝐶 → [𝐴 / 𝑥]𝐵 = 𝐶) → (([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶) → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)))
8	3, 5, 7	e11 39407	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)   )
9	8	in1 39281	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 = 𝐶 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1622   = wceq 1624   ∈ wcel 2131  [wsbc 3568  ⦋csb 3666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-sbc 3569  df-csb 3667  df-vd1 39280

This theorem is referenced by: (None)