Theorem csbsngVD 42402

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

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 42083	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		sbceqg 4340	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵))
3	1, 2	e1a 42136	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
4		csbconstg 3847	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝑦 = 𝑦)
5	1, 4	e1a 42136	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌𝑦 = 𝑦   )
6		eqeq1 2742	. . . . . . . . 9 ⊢ (⦋𝐴 / 𝑥⦌𝑦 = 𝑦 → (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵))
7	5, 6	e1a 42136	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
8		bibi1 351	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) ↔ (⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)))
9	8	biimprd 247	. . . . . . . 8 ⊢ (([𝐴 / 𝑥]𝑦 = 𝐵 ↔ ⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌𝑦 = ⦋𝐴 / 𝑥⦌𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)))
10	3, 7, 9	e11 42197	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
11	10	gen11 42125	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵)   )
12		abbi 2811	. . . . . . 7 ⊢ (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵})
13	12	biimpi 215	. . . . . 6 ⊢ (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵 ↔ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵) → {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵})
14	11, 13	e1a 42136	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
15		csbab 4368	. . . . . . . 8 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵}
16	15	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵})
17	16	eqcomd 2744	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵})
18	1, 17	e1a 42136	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   {𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
19		eqeq1 2742	. . . . . 6 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
20	19	biimpcd 248	. . . . 5 ⊢ ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ({𝑦 ∣ [𝐴 / 𝑥]𝑦 = 𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
21	14, 18, 20	e11 42197	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
22		df-sn 4559	. . . . . 6 ⊢ {𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
23	22	ax-gen 1799	. . . . 5 ⊢ ∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵}
24		csbeq2 3833	. . . . . 6 ⊢ (∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵})
25	24	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥{𝐵} = {𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}))
26	1, 23, 25	e10 42203	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵}   )
27		eqeq2 2750	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
28	27	biimpd 228	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝑦 = 𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
29	21, 26, 28	e11 42197	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}   )
30		df-sn 4559	. . 3 ⊢ {⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}
31		eqeq2 2750	. . . 4 ⊢ ({⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → (⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵} ↔ ⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵}))
32	31	biimprcd 249	. . 3 ⊢ (⦋𝐴 / 𝑥⦌{𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ({⦋𝐴 / 𝑥⦌𝐵} = {𝑦 ∣ 𝑦 = ⦋𝐴 / 𝑥⦌𝐵} → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}))
33	29, 30, 32	e10 42203	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}   )
34	33	in1 42080	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2108  {cab 2715  [wsbc 3711  ⦋csb 3828  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-nul 4254  df-sn 4559  df-vd1 42079

This theorem is referenced by: (None)