Theorem elrnmpt 5293

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∃wrex 2897   ↦ cmpt 4643  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  elrnmpt1s  5294  onnseq  7328  oarec  7529  fifo  8221  infpwfien  8768  fin23lem38  9054  fin1a2lem13  9117  ac6num  9184  isercoll2  14247  iserodd  15378  gsumwspan  17206  odf1o2  17811  mplcoe5lem  19288  neitr  20794  ordtbas2  20805  ordtopn1  20808  ordtopn2  20809  pnfnei  20834  mnfnei  20835  pnrmcld  20956  2ndcomap  21071  dis2ndc  21073  ptpjopn  21225  fbasrn  21498  elfm  21561  rnelfmlem  21566  rnelfm  21567  fmfnfmlem3  21570  fmfnfmlem4  21571  fmfnfm  21572  ptcmplem2  21667  tsmsfbas  21741  ustuqtoplem  21853  utopsnneiplem  21861  utopsnnei  21863  utopreg  21866  fmucnd  21906  neipcfilu  21910  imasdsf1olem  21988  xpsdsval  21996  met1stc  22136  metustel  22165  metustsym  22170  metuel2  22180  metustbl  22181  restmetu  22185  xrtgioo  22417  minveclem3b  23007  uniioombllem3  23159  dvivth  23577  gausslemma2dlem1a  24890  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  locfinreflem  29235  ordtconlem1  29298  esumcst  29452  esumrnmpt2  29457  measdivcstOLD  29614  oms0  29686  omssubadd  29689  cvmsss2  30510  poimirlem16  32595  poimirlem19  32598  poimirlem24  32603  poimirlem27  32606  itg2addnclem2  32632  nelrnmpt  38283  suprnmpt  38350  rnmptpr  38353  elrnmptd  38361  rnmptssrn  38363  wessf1ornlem  38366  disjrnmpt2  38370  disjf1o  38373  disjinfi  38375  choicefi  38387  stoweidlem27  38920  stoweidlem31  38924  stoweidlem35  38928  stirlinglem5  38971  stirlinglem13  38979  fourierdlem53  39052  fourierdlem80  39079  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  subsaliuncllem  39251  subsaliuncl  39252  sge0rnn0  39261  sge00  39269  fsumlesge0  39270  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0fsum  39280  sge0supre  39282  sge0rnbnd  39286  sge0pnffigt  39289  sge0lefi  39291  sge0ltfirp  39293  sge0resplit  39299  sge0split  39302  sge0reuz  39340  sge0reuzb  39341  hoidmvlelem2  39486