Theorem elrnmpt 5955

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.

Step	Hyp	Ref	Expression
1		eqeq1 2735	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵))
2	1	rexbidv 3177	. 2 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	rnmpt 5954	. 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	2, 4	elab2g 3670	1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  ∃wrex 3069   ↦ cmpt 5231  ran crn 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  elrnmpt1s  5956  elrnmptd  5960  elrnmptdv  5961  elrnmpt2d  5962  onnseq  8350  oarec  8568  fifo  9433  infpwfien  10063  fin23lem38  10350  fin1a2lem13  10413  ac6num  10480  isercoll2  15622  iserodd  16775  gsumwspan  18766  odf1o2  19486  mplcoe5lem  21818  neitr  22917  ordtbas2  22928  ordtopn1  22931  ordtopn2  22932  pnfnei  22957  mnfnei  22958  pnrmcld  23079  2ndcomap  23195  dis2ndc  23197  ptpjopn  23349  fbasrn  23621  elfm  23684  rnelfmlem  23689  rnelfm  23690  fmfnfmlem3  23693  fmfnfmlem4  23694  fmfnfm  23695  ptcmplem2  23790  tsmsfbas  23865  ustuqtoplem  23977  utopsnneiplem  23985  utopsnnei  23987  utopreg  23990  fmucnd  24030  neipcfilu  24034  imasdsf1olem  24112  xpsdsval  24120  met1stc  24263  metustel  24292  metustsym  24297  metuel2  24307  metustbl  24308  restmetu  24312  xrtgioo  24555  minveclem3b  25189  uniioombllem3  25347  dvivth  25776  gausslemma2dlem1a  27119  elimampt  32144  acunirnmpt  32166  acunirnmpt2  32167  acunirnmpt2f  32168  fnpreimac  32178  trsp2cyc  32567  nsgqusf1olem2  32814  nsgqusf1olem3  32815  locfinreflem  33133  zarclsint  33165  zarcls  33167  ordtconnlem1  33217  esumcst  33374  esumrnmpt2  33379  measdivcstALTV  33536  oms0  33609  omssubadd  33612  cvmsss2  34578  poimirlem16  36820  poimirlem19  36823  poimirlem24  36828  poimirlem27  36831  itg2addnclem2  36856  nelrnmpt  44087  suprnmpt  44184  rnmptpr  44187  wessf1ornlem  44195  disjrnmpt2  44198  disjf1o  44201  disjinfi  44202  choicefi  44210  rnmptlb  44258  rnmptbddlem  44259  rnmptbd2lem  44263  infnsuprnmpt  44265  elmptima  44273  supxrleubrnmpt  44427  suprleubrnmpt  44443  infrnmptle  44444  infxrunb3rnmpt  44449  supminfrnmpt  44466  infxrgelbrnmpt  44475  infrpgernmpt  44486  supminfxrrnmpt  44492  stoweidlem27  45054  stoweidlem31  45058  stoweidlem35  45062  stirlinglem5  45105  stirlinglem13  45113  fourierdlem80  45213  fourierdlem93  45226  fourierdlem103  45236  fourierdlem104  45237  subsaliuncllem  45384  subsaliuncl  45385  sge0rnn0  45395  sge00  45403  fsumlesge0  45404  sge0tsms  45407  sge0cl  45408  sge0f1o  45409  sge0fsum  45414  sge0supre  45416  sge0rnbnd  45420  sge0pnffigt  45423  sge0lefi  45425  sge0ltfirp  45427  sge0resplit  45433  sge0split  45436  sge0reuz  45474  sge0reuzb  45475  hoidmvlelem2  45623  smfpimcc  45835