Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbresgVD Structured version   Visualization version   GIF version

Theorem csbresgVD 39547
Description: Virtual deduction proof of csbresgOLD 39472. 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. csbresgOLD 39472 is csbresgVD 39547 without virtual deductions and was automatically derived from csbresgVD 39547.
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
StepHypRef Expression
1 idn1 39209 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 csbconstg 3652 . . . . . . . . 9 (𝐴𝑉𝐴 / 𝑥V = V)
31, 2e1a 39271 . . . . . . . 8 (   𝐴𝑉   ▶   𝐴 / 𝑥V = V   )
4 xpeq2 5238 . . . . . . . 8 (𝐴 / 𝑥V = V → (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V))
53, 4e1a 39271 . . . . . . 7 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V)   )
6 csbxpgOLD 39470 . . . . . . . 8 (𝐴𝑉𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V))
71, 6e1a 39271 . . . . . . 7 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V)   )
8 eqeq2 2735 . . . . . . . 8 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) ↔ 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
98biimpd 219 . . . . . . 7 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) → 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
105, 7, 9e11 39332 . . . . . 6 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)   )
11 ineq2 3916 . . . . . 6 (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)))
1210, 11e1a 39271 . . . . 5 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
13 csbingOLD 39471 . . . . . 6 (𝐴𝑉𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)))
141, 13e1a 39271 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V))   )
15 eqeq2 2735 . . . . . 6 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1615biimpd 219 . . . . 5 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) → 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1712, 14, 16e11 39332 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
18 df-res 5230 . . . . . 6 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
1918ax-gen 1835 . . . . 5 𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
20 csbeq2gOLD 39184 . . . . 5 (𝐴𝑉 → (∀𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))))
211, 19, 20e10 39338 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))   )
22 eqeq2 2735 . . . . 5 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2322biimpd 219 . . . 4 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2417, 21, 23e11 39332 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
25 df-res 5230 . . 3 (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))
26 eqeq2 2735 . . . 4 ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2726biimprcd 240 . . 3 (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)))
2824, 25, 27e10 39338 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)   )
2928in1 39206 1 (𝐴𝑉𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1594   = wceq 1596  wcel 2103  Vcvv 3304  csb 3639  cin 3679   × cxp 5216  cres 5220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-in 3687  df-nul 4024  df-opab 4821  df-xp 5224  df-res 5230  df-vd1 39205
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator