Theorem csbsngVD 45466

Description: Virtual deduction proof of csbsng 4670. 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. csbsng 4670 is csbsngVD 45466 without virtual deductions and was automatically derived from csbsngVD 45466.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
3:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑦 = 𝑦   )
4:3:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
5:2,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
7:6:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
8:1:	⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
9:7,8:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
10::	⊢ {𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
11:10:	⊢ ∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
12:1,11:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = ⦋ 𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
13:9,12:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { 𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
14::	⊢ {⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}
15:13,14:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = { ⦋𝐴 / 𝑥⦌𝐵}   )
qed:15:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋ 𝐴 / 𝑥⦌𝐵})

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

Assertion

Ref	Expression
csbsngVD	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})

Proof of Theorem csbsngVD

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 45148	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		sbceqg 4369	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵))
3	1, 2	e1a 45201	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
4		csbconstg 3874	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
5	1, 4	e1a 45201	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑦 = 𝑦   )
6		eqeq1 2769	. . . . . . . . 9 ⊢ (⦋𝐴 / 𝑥⦌𝑦 = 𝑦 → (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵))
7	5, 6	e1a 45201	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
8		bibi1 354	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) ↔ (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)))
9	8	biimprd 251	. . . . . . . 8 ⊢ (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)))
10	3, 7, 9	e11 45262	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
11	10	gen11 45190	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
12		abbib 2834	. . . . . . 7 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} ↔ ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵))
13	12	biimpri 231	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵})
14	11, 13	e1a 45201	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
15		csbab 4397	. . . . . . . 8 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵}
16	15	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵})
17	16	eqcomd 2771	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵})
18	1, 17	e1a 45201	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
19		eqeq1 2769	. . . . . 6 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
20	19	biimpcd 252	. . . . 5 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
21	14, 18, 20	e11 45262	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
22		df-sn 4586	. . . . . 6 ⊢ {𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
23	22	ax-gen 1818	. . . . 5 ⊢ ∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
24		csbeq2 3860	. . . . . 6 ⊢ (∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵})
25	24	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}))
26	1, 23, 25	e10 45268	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
27		eqeq2 2777	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
28	27	biimpd 232	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
29	21, 26, 28	e11 45262	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
30		df-sn 4586	. . 3 ⊢ {⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}
31		eqeq2 2777	. . . 4 ⊢ ({⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
32	31	biimprcd 253	. . 3 ⊢ (⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ({⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}))
33	29, 30, 32	e10 45268	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}   )
34	33	in1 45145	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747  ⦋csb 3855  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-nul 4289  df-sn 4586  df-vd1 45144

This theorem is referenced by: (None)