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 41106
Description: Virtual deduction proof of csbres 5849. 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 5849 is csbresgVD 41106 without virtual deductions and was automatically derived from csbresgVD 41106.
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 40785 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 csbconstg 3899 . . . . . . . . 9 (𝐴𝑉𝐴 / 𝑥V = V)
31, 2e1a 40838 . . . . . . . 8 (   𝐴𝑉   ▶   𝐴 / 𝑥V = V   )
4 xpeq2 5569 . . . . . . . 8 (𝐴 / 𝑥V = V → (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V))
53, 4e1a 40838 . . . . . . 7 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V)   )
6 csbxp 5643 . . . . . . . . 9 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V)
76a1i 11 . . . . . . . 8 (𝐴𝑉𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V))
81, 7e1a 40838 . . . . . . 7 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V)   )
9 eqeq2 2830 . . . . . . . 8 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) ↔ 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
109biimpd 230 . . . . . . 7 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) → 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
115, 8, 10e11 40899 . . . . . 6 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)   )
12 ineq2 4180 . . . . . 6 (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)))
1311, 12e1a 40838 . . . . 5 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
14 csbin 4388 . . . . . . 7 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V))
1514a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)))
161, 15e1a 40838 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V))   )
17 eqeq2 2830 . . . . . 6 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1817biimpd 230 . . . . 5 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) → 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1913, 16, 18e11 40899 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
20 df-res 5560 . . . . . 6 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
2120ax-gen 1787 . . . . 5 𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
22 csbeq2 3885 . . . . . 6 (∀𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)))
2322a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))))
241, 21, 23e10 40905 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))   )
25 eqeq2 2830 . . . . 5 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2625biimpd 230 . . . 4 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2719, 24, 26e11 40899 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
28 df-res 5560 . . 3 (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))
29 eqeq2 2830 . . . 4 ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
3029biimprcd 251 . . 3 (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)))
3127, 28, 30e10 40905 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)   )
3231in1 40782 1 (𝐴𝑉𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526   = wceq 1528  wcel 2105  Vcvv 3492  csb 3880  cin 3932   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-in 3940  df-nul 4289  df-opab 5120  df-xp 5554  df-res 5560  df-vd1 40781
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator