Theorem elrnmpt 5907

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 2745	. . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐵 ↔ 𝐶 = 𝐵))
2	1	rexbidv 3165	. 2 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	rnmpt 5906	. 2 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}
5	2, 4	elab2g 3620	1 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ∃wrex 3065   ↦ cmpt 5156  ran crn 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-mpt 5157  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  elrnmpt1s  5908  elrnmptd  5912  elrnmptdv  5914  elrnmpt2d  5915  nelrnmpt  5916  elimampt  6002  onnseq  8278  oarec  8491  fifo  9339  infpwfien  9979  fin23lem38  10266  fin1a2lem13  10329  ac6num  10396  isercoll2  15626  iserodd  16801  gsumwspan  18809  odf1o2  19543  mplcoe5lem  22019  neitr  23167  ordtbas2  23178  ordtopn1  23181  ordtopn2  23182  pnfnei  23207  mnfnei  23208  pnrmcld  23329  2ndcomap  23445  dis2ndc  23447  ptpjopn  23599  fbasrn  23871  elfm  23934  rnelfmlem  23939  rnelfm  23940  fmfnfmlem3  23943  fmfnfmlem4  23944  fmfnfm  23945  ptcmplem2  24040  tsmsfbas  24115  ustuqtoplem  24226  utopsnneiplem  24234  utopsnnei  24236  utopreg  24239  fmucnd  24278  neipcfilu  24282  imasdsf1olem  24360  xpsdsval  24368  met1stc  24508  metustel  24537  metustsym  24542  metuel2  24552  metustbl  24553  restmetu  24557  xrtgioo  24794  minveclem3b  25417  uniioombllem3  25574  dvivth  25999  gausslemma2dlem1a  27350  acunirnmpt  32755  acunirnmpt2  32756  acunirnmpt2f  32757  fnpreimac  32766  trsp2cyc  33208  elrgspnlem1  33327  elrgspnlem2  33328  elrgspn  33331  nsgqusf1olem2  33501  nsgqusf1olem3  33502  locfinreflem  34036  zarclsint  34068  zarcls  34070  ordtconnlem1  34120  esumcst  34259  esumrnmpt2  34264  measdivcstALTV  34421  oms0  34493  omssubadd  34496  cvmsss2  35517  poimirlem16  38018  poimirlem19  38021  poimirlem24  38026  poimirlem27  38029  itg2addnclem2  38054  suprnmpt  45635  rnmptpr  45638  wessf1ornlem  45646  disjrnmpt2  45649  disjf1o  45652  disjinfi  45653  choicefi  45660  rnmptlb  45701  rnmptbddlem  45702  rnmptbd2lem  45706  infnsuprnmpt  45708  elmptima  45716  supxrleubrnmpt  45863  suprleubrnmpt  45879  infrnmptle  45880  infxrunb3rnmpt  45885  supminfrnmpt  45902  infxrgelbrnmpt  45911  infrpgernmpt  45922  supminfxrrnmpt  45928  stoweidlem27  46484  stoweidlem31  46488  stoweidlem35  46492  stirlinglem5  46535  stirlinglem13  46543  fourierdlem80  46643  fourierdlem93  46656  fourierdlem103  46666  fourierdlem104  46667  subsaliuncllem  46814  subsaliuncl  46815  sge0rnn0  46825  sge00  46833  fsumlesge0  46834  sge0tsms  46837  sge0cl  46838  sge0f1o  46839  sge0fsum  46844  sge0supre  46846  sge0rnbnd  46850  sge0pnffigt  46853  sge0lefi  46855  sge0ltfirp  46857  sge0resplit  46863  sge0split  46866  sge0reuz  46904  sge0reuzb  46905  hoidmvlelem2  47053  smfpimcc  47265