Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrnmpt1s Structured version   Visualization version   GIF version

Theorem elrnmpt1s 5803
 Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
Hypotheses
Ref Expression
rnmpt.1 𝐹 = (𝑥𝐴𝐵)
elrnmpt1s.1 (𝑥 = 𝐷𝐵 = 𝐶)
Assertion
Ref Expression
elrnmpt1s ((𝐷𝐴𝐶𝑉) → 𝐶 ∈ ran 𝐹)
Distinct variable groups:   𝑥,𝐶   𝑥,𝐴   𝑥,𝐷
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt1s
StepHypRef Expression
1 eqid 2758 . . 3 𝐶 = 𝐶
2 elrnmpt1s.1 . . . 4 (𝑥 = 𝐷𝐵 = 𝐶)
32rspceeqv 3558 . . 3 ((𝐷𝐴𝐶 = 𝐶) → ∃𝑥𝐴 𝐶 = 𝐵)
41, 3mpan2 690 . 2 (𝐷𝐴 → ∃𝑥𝐴 𝐶 = 𝐵)
5 rnmpt.1 . . . 4 𝐹 = (𝑥𝐴𝐵)
65elrnmpt 5802 . . 3 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
76biimparc 483 . 2 ((∃𝑥𝐴 𝐶 = 𝐵𝐶𝑉) → 𝐶 ∈ ran 𝐹)
84, 7sylan 583 1 ((𝐷𝐴𝐶𝑉) → 𝐶 ∈ ran 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071   ↦ cmpt 5116  ran crn 5529 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  ax-sep 5173  ax-nul 5180  ax-pr 5302 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-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-mpt 5117  df-cnv 5536  df-dm 5538  df-rn 5539 This theorem is referenced by:  wunex2  10211  dfod2  18772  dprd2dlem1  19245  dprd2da  19246  ordtbaslem  21902  subgntr  22821  opnsubg  22822  tgpconncomp  22827  tsmsxplem1  22867  xrge0gsumle  23548  xrge0tsms  23549  minveclem3b  24142  minveclem3  24143  minveclem4  24146  efsubm  25256  dchrisum0fno1  26208  fnpreimac  30545  xrge0tsmsd  30856  esumcvg  31586  esum2d  31593  msubco  33022  suprubrnmpt2  42303  infxrlbrnmpt2  42458  sge0xaddlem1  43483
 Copyright terms: Public domain W3C validator