Theorem elrnmpt 5949

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∃wrex 3095   ↦ cmpt 5196  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-mpt 5197  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  elrnmpt1s  5950  elrnmptd  5954  elrnmptdv  5956  elrnmpt2d  5957  nelrnmpt  5958  elimampt  6046  onnseq  8331  oarec  8547  fifo  9392  infpwfien  10046  fin23lem38  10333  fin1a2lem13  10396  ac6num  10463  isercoll2  15720  iserodd  16895  gsumwspan  18905  odf1o2  19643  mplcoe5lem  22159  neitr  23306  ordtbas2  23317  ordtopn1  23320  ordtopn2  23321  pnfnei  23346  mnfnei  23347  pnrmcld  23468  2ndcomap  23584  dis2ndc  23586  ptpjopn  23738  fbasrn  24010  elfm  24073  rnelfmlem  24078  rnelfm  24079  fmfnfmlem3  24082  fmfnfmlem4  24083  fmfnfm  24084  ptcmplem2  24179  tsmsfbas  24254  ustuqtoplem  24365  utopsnneiplem  24373  utopsnnei  24375  utopreg  24378  fmucnd  24417  neipcfilu  24421  imasdsf1olem  24499  xpsdsval  24507  met1stc  24647  metustel  24676  metustsym  24681  metuel2  24691  metustbl  24692  restmetu  24696  xrtgioo  24933  minveclem3b  25556  uniioombllem3  25713  dvivth  26138  gausslemma2dlem1a  27495  acunirnmpt  32945  acunirnmpt2  32946  acunirnmpt2f  32947  fnpreimac  32956  trsp2cyc  33384  elrgspnlem1  33503  elrgspnlem2  33504  elrgspn  33507  nsgqusf1olem2  33667  nsgqusf1olem3  33668  locfinreflem  34175  zarclsint  34207  zarcls  34209  ordtconnlem1  34259  esumcst  34398  esumrnmpt2  34403  measdivcstALTV  34560  oms0  34632  omssubadd  34635  cvmsss2  35699  poimirlem16  38209  poimirlem19  38212  poimirlem24  38217  poimirlem27  38220  itg2addnclem2  38245  suprnmpt  45818  rnmptpr  45821  wessf1ornlem  45829  disjrnmpt2  45832  disjf1o  45835  disjinfi  45836  choicefi  45843  rnmptlb  45884  rnmptbddlem  45885  rnmptbd2lem  45889  infnsuprnmpt  45891  elmptima  45899  supxrleubrnmpt  46046  suprleubrnmpt  46062  infrnmptle  46063  infxrunb3rnmpt  46068  supminfrnmpt  46085  infxrgelbrnmpt  46094  infrpgernmpt  46105  supminfxrrnmpt  46111  stoweidlem27  46667  stoweidlem31  46671  stoweidlem35  46675  stirlinglem5  46718  stirlinglem13  46726  fourierdlem80  46826  fourierdlem93  46839  fourierdlem103  46849  fourierdlem104  46850  subsaliuncllem  46997  subsaliuncl  46998  sge0rnn0  47008  sge00  47016  fsumlesge0  47017  sge0tsms  47020  sge0cl  47021  sge0f1o  47022  sge0fsum  47027  sge0supre  47029  sge0rnbnd  47033  sge0pnffigt  47036  sge0lefi  47038  sge0ltfirp  47040  sge0resplit  47046  sge0split  47049  sge0reuz  47087  sge0reuzb  47088  hoidmvlelem2  47236  smfpimcc  47448