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

Theorem csbima12gALTVD 44483
Description: Virtual deduction proof of csbima12 6083. 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. csbima12 6083 is csbima12gALTVD 44483 without virtual deductions and was automatically derived from csbima12gALTVD 44483.
1:: (   𝐴𝐶   ▶   𝐴𝐶   )
2:1: (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = ( 𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
3:2: (   𝐴𝐶   ▶    ran 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
4:1: (   𝐴𝐶   ▶    𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵)   )
5:3,4: (   𝐴𝐶   ▶    𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
6:: (𝐹𝐵) = ran (𝐹𝐵)
7:6: 𝑥(𝐹𝐵) = ran (𝐹𝐵)
8:1,7: (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵)   )
9:5,8: (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
10:: (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)
11:9,10: (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = ( 𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
qed:11: (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = ( 𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbima12gALTVD (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))

Proof of Theorem csbima12gALTVD
StepHypRef Expression
1 idn1 44160 . . . . . . 7 (   𝐴𝐶   ▶   𝐴𝐶   )
2 csbres 5988 . . . . . . . 8 𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)
32a1i 11 . . . . . . 7 (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
41, 3e1a 44213 . . . . . 6 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
5 rneq 5938 . . . . . 6 (𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → ran 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
64, 5e1a 44213 . . . . 5 (   𝐴𝐶   ▶   ran 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
7 csbrn 6209 . . . . . . 7 𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵)
87a1i 11 . . . . . 6 (𝐴𝐶𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵))
91, 8e1a 44213 . . . . 5 (   𝐴𝐶   ▶   𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵)   )
10 eqeq2 2737 . . . . . 6 (ran 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → (𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵) ↔ 𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
1110biimpd 228 . . . . 5 (ran 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → (𝐴 / 𝑥ran (𝐹𝐵) = ran 𝐴 / 𝑥(𝐹𝐵) → 𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
126, 9, 11e11 44274 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
13 df-ima 5691 . . . . . 6 (𝐹𝐵) = ran (𝐹𝐵)
1413ax-gen 1789 . . . . 5 𝑥(𝐹𝐵) = ran (𝐹𝐵)
15 csbeq2 3894 . . . . . 6 (∀𝑥(𝐹𝐵) = ran (𝐹𝐵) → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵))
1615a1i 11 . . . . 5 (𝐴𝐶 → (∀𝑥(𝐹𝐵) = ran (𝐹𝐵) → 𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵)))
171, 14, 16e10 44280 . . . 4 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵)   )
18 eqeq2 2737 . . . . 5 (𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵) ↔ 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
1918biimpd 228 . . . 4 (𝐴 / 𝑥ran (𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → (𝐴 / 𝑥(𝐹𝐵) = 𝐴 / 𝑥ran (𝐹𝐵) → 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
2012, 17, 19e11 44274 . . 3 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
21 df-ima 5691 . . 3 (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)
22 eqeq2 2737 . . . 4 ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → (𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) ↔ 𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
2322biimprcd 249 . . 3 (𝐴 / 𝑥(𝐹𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) = ran (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵) → 𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)))
2420, 21, 23e10 44280 . 2 (   𝐴𝐶   ▶   𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵)   )
2524in1 44157 1 (𝐴𝐶𝐴 / 𝑥(𝐹𝐵) = (𝐴 / 𝑥𝐹𝐴 / 𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531   = wceq 1533  wcel 2098  csb 3889  ran crn 5679  cres 5680  cima 5681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-rel 5685  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-vd1 44156
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator