Theorem csbresgVD 41974

Description: Virtual deduction proof of csbres 5826. 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. csbres 5826 is csbresgVD 41974 without virtual deductions and was automatically derived from csbresgVD 41974.

1::	⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌V = V   )
3:2:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
4:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)   )
5:3,4:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
6:5:	⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
7:1:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))   )
8:6,7:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
9::	⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
10:9:	⊢ ∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
11:1,10:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))   )
12:8,11:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
13::	⊢ (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))
14:12,13:	⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)   )
qed:14:	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ( ⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))

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

Assertion

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

Proof of Theorem csbresgVD

Step	Hyp	Ref	Expression
1		idn1 41653	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		csbconstg 3824	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌V = V)
3	1, 2	e1a 41706	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌V = V   )
4		xpeq2 5545	. . . . . . . 8 ⊢ (⦋𝐴 / 𝑥⦌V = V → (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V))
5	3, 4	e1a 41706	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
6		csbxp 5619	. . . . . . . . 9 ⊢ ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V))
8	1, 7	e1a 41706	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)   )
9		eqeq2 2770	. . . . . . . 8 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) ↔ ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)))
10	9	biimpd 232	. . . . . . 7 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) → ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)))
11	5, 8, 10	e11 41767	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
12		ineq2 4111	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)))
13	11, 12	e1a 41706	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
14		csbin 4336	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))
15	14	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)))
16	1, 15	e1a 41706	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))   )
17		eqeq2 2770	. . . . . 6 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
18	17	biimpd 232	. . . . 5 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
19	13, 16, 18	e11 41767	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
20		df-res 5536	. . . . . 6 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
21	20	ax-gen 1797	. . . . 5 ⊢ ∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
22		csbeq2 3810	. . . . . 6 ⊢ (∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)))
23	22	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))))
24	1, 21, 23	e10 41773	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))   )
25		eqeq2 2770	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
26	25	biimpd 232	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
27	19, 24, 26	e11 41767	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
28		df-res 5536	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))
29		eqeq2 2770	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
30	29	biimprcd 253	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → ((⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)))
31	27, 28, 30	e10 41773	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)   )
32	31	in1 41650	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4  ∀wal 1536   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ⦋csb 3805   ∩ cin 3857   × cxp 5522   ↾ cres 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-in 3865  df-nul 4226  df-opab 5095  df-xp 5530  df-res 5536  df-vd1 41649

This theorem is referenced by: (None)