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

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
StepHypRef Expression
1 idn1 41653 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 csbconstg 3824 . . . . . . . . 9 (𝐴𝑉𝐴 / 𝑥V = V)
31, 2e1a 41706 . . . . . . . 8 (   𝐴𝑉   ▶   𝐴 / 𝑥V = V   )
4 xpeq2 5545 . . . . . . . 8 (𝐴 / 𝑥V = V → (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V))
53, 4e1a 41706 . . . . . . 7 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V)   )
6 csbxp 5619 . . . . . . . . 9 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V)
76a1i 11 . . . . . . . 8 (𝐴𝑉𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V))
81, 7e1a 41706 . . . . . . 7 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V)   )
9 eqeq2 2770 . . . . . . . 8 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) ↔ 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
109biimpd 232 . . . . . . 7 ((𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × 𝐴 / 𝑥V) → 𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)))
115, 8, 10e11 41767 . . . . . 6 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V)   )
12 ineq2 4111 . . . . . 6 (𝐴 / 𝑥(𝐶 × V) = (𝐴 / 𝑥𝐶 × V) → (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)))
1311, 12e1a 41706 . . . . 5 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
14 csbin 4336 . . . . . . 7 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V))
1514a1i 11 . . . . . 6 (𝐴𝑉𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)))
161, 15e1a 41706 . . . . 5 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V))   )
17 eqeq2 2770 . . . . . 6 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1817biimpd 232 . . . . 5 ((𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵𝐴 / 𝑥(𝐶 × V)) → 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
1913, 16, 18e11 41767 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
20 df-res 5536 . . . . . 6 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
2120ax-gen 1797 . . . . 5 𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
22 csbeq2 3810 . . . . . 6 (∀𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)))
2322a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥(𝐵𝐶) = (𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))))
241, 21, 23e10 41773 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V))   )
25 eqeq2 2770 . . . . 5 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2625biimpd 232 . . . 4 (𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = 𝐴 / 𝑥(𝐵 ∩ (𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
2719, 24, 26e11 41767 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))   )
28 df-res 5536 . . 3 (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))
29 eqeq2 2770 . . . 4 ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) ↔ 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V))))
3029biimprcd 253 . . 3 (𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → ((𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶) = (𝐴 / 𝑥𝐵 ∩ (𝐴 / 𝑥𝐶 × V)) → 𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)))
3127, 28, 30e10 41773 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶)   )
3231in1 41650 1 (𝐴𝑉𝐴 / 𝑥(𝐵𝐶) = (𝐴 / 𝑥𝐵𝐴 / 𝑥𝐶))
 Colors of variables: wff setvar class 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)
 Copyright terms: Public domain W3C validator