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

Theorem elrnmpt 5361
Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
Hypothesis
Ref Expression
rnmpt.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
elrnmpt (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2624 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐵𝐶 = 𝐵))
21rexbidv 3048 . 2 (𝑦 = 𝐶 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43rnmpt 5360 . 2 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
52, 4elab2g 3347 1 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  wrex 2910  cmpt 4720  ran crn 5105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-mpt 4721  df-cnv 5112  df-dm 5114  df-rn 5115
This theorem is referenced by:  elrnmpt1s  5362  onnseq  7426  oarec  7627  fifo  8323  infpwfien  8870  fin23lem38  9156  fin1a2lem13  9219  ac6num  9286  isercoll2  14380  iserodd  15521  gsumwspan  17364  odf1o2  17969  mplcoe5lem  19448  neitr  20965  ordtbas2  20976  ordtopn1  20979  ordtopn2  20980  pnfnei  21005  mnfnei  21006  pnrmcld  21127  2ndcomap  21242  dis2ndc  21244  ptpjopn  21396  fbasrn  21669  elfm  21732  rnelfmlem  21737  rnelfm  21738  fmfnfmlem3  21741  fmfnfmlem4  21742  fmfnfm  21743  ptcmplem2  21838  tsmsfbas  21912  ustuqtoplem  22024  utopsnneiplem  22032  utopsnnei  22034  utopreg  22037  fmucnd  22077  neipcfilu  22081  imasdsf1olem  22159  xpsdsval  22167  met1stc  22307  metustel  22336  metustsym  22341  metuel2  22351  metustbl  22352  restmetu  22356  xrtgioo  22590  minveclem3b  23180  uniioombllem3  23334  dvivth  23754  gausslemma2dlem1a  25071  elimampt  29411  acunirnmpt  29432  acunirnmpt2  29433  acunirnmpt2f  29434  locfinreflem  29881  ordtconnlem1  29944  esumcst  30099  esumrnmpt2  30104  measdivcstOLD  30261  oms0  30333  omssubadd  30336  cvmsss2  31230  poimirlem16  33396  poimirlem19  33399  poimirlem24  33404  poimirlem27  33407  itg2addnclem2  33433  nelrnmpt  39077  suprnmpt  39171  rnmptpr  39174  elrnmptd  39182  rnmptssrn  39184  wessf1ornlem  39187  disjrnmpt2  39191  disjf1o  39194  disjinfi  39196  choicefi  39208  rnmptlb  39269  rnmptbddlem  39271  rnmptbd2lem  39279  infnsuprnmpt  39281  elmptima  39289  supxrleubrnmpt  39445  suprleubrnmpt  39462  infrnmptle  39463  infxrunb3rnmpt  39468  supminfrnmpt  39485  infxrgelbrnmpt  39496  infrpgernmpt  39508  supminfxrrnmpt  39514  stoweidlem27  40007  stoweidlem31  40011  stoweidlem35  40015  stirlinglem5  40058  stirlinglem13  40066  fourierdlem53  40139  fourierdlem80  40166  fourierdlem93  40179  fourierdlem103  40189  fourierdlem104  40190  subsaliuncllem  40338  subsaliuncl  40339  sge0rnn0  40348  sge00  40356  fsumlesge0  40357  sge0tsms  40360  sge0cl  40361  sge0f1o  40362  sge0fsum  40367  sge0supre  40369  sge0rnbnd  40373  sge0pnffigt  40376  sge0lefi  40378  sge0ltfirp  40380  sge0resplit  40386  sge0split  40389  sge0reuz  40427  sge0reuzb  40428  hoidmvlelem2  40573  smfpimcc  40777
  Copyright terms: Public domain W3C validator