Theorem csbresgVD 45338

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

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 45018	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝑉   ▶   𝐴 ∈ 𝑉   )
2		csbconstg 3850	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌V = V)
3	1, 2	e1a 45071	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌V = V   )
4		xpeq2 5639	. . . . . . . 8 ⊢ (⦋𝐴 / 𝑥⦌V = V → (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V))
5	3, 4	e1a 45071	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
6		csbxp 5719	. . . . . . . . 9 ⊢ ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)
7	6	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V))
8	1, 7	e1a 45071	. . . . . . 7 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V)   )
9		eqeq2 2751	. . . . . . . 8 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) ↔ ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)))
10	9	biimpd 230	. . . . . . 7 ⊢ ((⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × ⦋𝐴 / 𝑥⦌V) → ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)))
11	5, 8, 10	e11 45132	. . . . . 6 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V)   )
12		ineq2 4143	. . . . . 6 ⊢ (⦋𝐴 / 𝑥⦌(𝐶 × V) = (⦋𝐴 / 𝑥⦌𝐶 × V) → (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)))
13	11, 12	e1a 45071	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
14		csbin 4370	. . . . . . 7 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))
15	14	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)))
16	1, 15	e1a 45071	. . . . 5 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V))   )
17		eqeq2 2751	. . . . . 6 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
18	17	biimpd 230	. . . . 5 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ ⦋𝐴 / 𝑥⦌(𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
19	13, 16, 18	e11 45132	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
20		df-res 5630	. . . . . 6 ⊢ (𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
21	20	ax-gen 1802	. . . . 5 ⊢ ∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V))
22		csbeq2 3836	. . . . . 6 ⊢ (∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)))
23	22	a1i 11	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝐵 ↾ 𝐶) = (𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))))
24	1, 21, 23	e10 45138	. . . 4 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V))   )
25		eqeq2 2751	. . . . 5 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
26	25	biimpd 230	. . . 4 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∩ (𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
27	19, 24, 26	e11 45132	. . 3 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))   )
28		df-res 5630	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))
29		eqeq2 2751	. . . 4 ⊢ ((⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V))))
30	29	biimprcd 251	. . 3 ⊢ (⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → ((⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∩ (⦋𝐴 / 𝑥⦌𝐶 × V)) → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)))
31	27, 28, 30	e10 45138	. 2 ⊢ (   𝐴 ∈ 𝑉   ▶   ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶)   )
32	31	in1 45015	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4  ∀wal 1545   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ⦋csb 3831   ∩ cin 3882   × cxp 5616   ↾ cres 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-in 3890  df-nul 4262  df-opab 5135  df-xp 5624  df-res 5630  df-vd1 45014

This theorem is referenced by: (None)