Theorem elrnmpt 5950

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ∃wrex 3091   ↦ cmpt 5194  ran crn 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  elrnmpt1s  5951  elrnmptd  5955  elrnmptdv  5957  elrnmpt2d  5958  nelrnmpt  5959  elimampt  6047  onnseq  8337  oarec  8553  fifo  9399  infpwfien  10062  fin23lem38  10348  fin1a2lem13  10411  ac6num  10478  isercoll2  15748  iserodd  16921  gsumwspan  18946  odf1o2  19691  mplcoe5lem  22244  neitr  23391  ordtbas2  23402  ordtopn1  23405  ordtopn2  23406  pnfnei  23431  mnfnei  23432  pnrmcld  23553  2ndcomap  23670  dis2ndc  23672  ptpjopn  23824  fbasrn  24096  elfm  24159  rnelfmlem  24164  rnelfm  24165  fmfnfmlem3  24168  fmfnfmlem4  24169  fmfnfm  24170  ptcmplem2  24265  tsmsfbas  24340  ustuqtoplem  24451  utopsnneiplem  24459  utopsnnei  24461  utopreg  24464  fmucnd  24503  neipcfilu  24507  imasdsf1olem  24585  xpsdsval  24593  met1stc  24733  metustel  24762  metustsym  24767  metuel2  24777  metustbl  24778  restmetu  24782  xrtgioo  25019  minveclem3b  25642  uniioombllem3  25799  dvivth  26224  gausslemma2dlem1a  27584  acunirnmpt  33079  acunirnmpt2  33080  acunirnmpt2f  33081  fnpreimac  33090  trsp2cyc  33511  elrgspnlem1  33630  elrgspnlem2  33631  elrgspn  33634  nsgqusf1olem2  33791  nsgqusf1olem3  33792  locfinreflem  34298  zarclsint  34330  zarcls  34332  ordtconnlem1  34382  esumcst  34521  esumrnmpt2  34526  measdivcstALTV  34684  oms0  34756  omssubadd  34759  cvmsss2  35807  poimirlem16  38348  poimirlem19  38351  poimirlem24  38356  poimirlem27  38359  itg2addnclem2  38384  suprnmpt  45969  rnmptpr  45972  wessf1ornlem  45980  disjrnmpt2  45983  disjf1o  45986  disjinfi  45987  choicefi  45994  rnmptlb  46035  rnmptbddlem  46036  rnmptbd2lem  46040  infnsuprnmpt  46042  elmptima  46050  supxrleubrnmpt  46197  suprleubrnmpt  46213  infrnmptle  46214  infxrunb3rnmpt  46219  supminfrnmpt  46236  infxrgelbrnmpt  46245  infrpgernmpt  46256  supminfxrrnmpt  46262  stoweidlem27  46818  stoweidlem31  46822  stoweidlem35  46826  stirlinglem5  46869  stirlinglem13  46877  fourierdlem80  46977  fourierdlem93  46990  fourierdlem103  47000  fourierdlem104  47001  subsaliuncllem  47148  subsaliuncl  47149  sge0rnn0  47159  sge00  47167  fsumlesge0  47168  sge0tsms  47171  sge0cl  47172  sge0f1o  47173  sge0fsum  47178  sge0supre  47180  sge0rnbnd  47184  sge0pnffigt  47187  sge0lefi  47189  sge0ltfirp  47191  sge0resplit  47197  sge0split  47200  sge0reuz  47238  sge0reuzb  47239  hoidmvlelem2  47387  smfpimcc  47599