Theorem elrnmpt 5972

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  ∃wrex 3068   ↦ cmpt 5231  ran crn 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  elrnmpt1s  5973  elrnmptd  5977  elrnmptdv  5979  elrnmpt2d  5980  elimampt  6063  onnseq  8383  oarec  8599  fifo  9470  infpwfien  10100  fin23lem38  10387  fin1a2lem13  10450  ac6num  10517  isercoll2  15702  iserodd  16869  gsumwspan  18872  odf1o2  19606  mplcoe5lem  22075  neitr  23204  ordtbas2  23215  ordtopn1  23218  ordtopn2  23219  pnfnei  23244  mnfnei  23245  pnrmcld  23366  2ndcomap  23482  dis2ndc  23484  ptpjopn  23636  fbasrn  23908  elfm  23971  rnelfmlem  23976  rnelfm  23977  fmfnfmlem3  23980  fmfnfmlem4  23981  fmfnfm  23982  ptcmplem2  24077  tsmsfbas  24152  ustuqtoplem  24264  utopsnneiplem  24272  utopsnnei  24274  utopreg  24277  fmucnd  24317  neipcfilu  24321  imasdsf1olem  24399  xpsdsval  24407  met1stc  24550  metustel  24579  metustsym  24584  metuel2  24594  metustbl  24595  restmetu  24599  xrtgioo  24842  minveclem3b  25476  uniioombllem3  25634  dvivth  26064  gausslemma2dlem1a  27424  acunirnmpt  32676  acunirnmpt2  32677  acunirnmpt2f  32678  fnpreimac  32688  trsp2cyc  33126  elrgspnlem1  33232  elrgspnlem2  33233  elrgspn  33236  nsgqusf1olem2  33422  nsgqusf1olem3  33423  locfinreflem  33801  zarclsint  33833  zarcls  33835  ordtconnlem1  33885  esumcst  34044  esumrnmpt2  34049  measdivcstALTV  34206  oms0  34279  omssubadd  34282  cvmsss2  35259  poimirlem16  37623  poimirlem19  37626  poimirlem24  37631  poimirlem27  37634  itg2addnclem2  37659  nelrnmpt  45024  suprnmpt  45117  rnmptpr  45120  wessf1ornlem  45128  disjrnmpt2  45131  disjf1o  45134  disjinfi  45135  choicefi  45143  rnmptlb  45188  rnmptbddlem  45189  rnmptbd2lem  45193  infnsuprnmpt  45195  elmptima  45203  supxrleubrnmpt  45356  suprleubrnmpt  45372  infrnmptle  45373  infxrunb3rnmpt  45378  supminfrnmpt  45395  infxrgelbrnmpt  45404  infrpgernmpt  45415  supminfxrrnmpt  45421  stoweidlem27  45983  stoweidlem31  45987  stoweidlem35  45991  stirlinglem5  46034  stirlinglem13  46042  fourierdlem80  46142  fourierdlem93  46155  fourierdlem103  46165  fourierdlem104  46166  subsaliuncllem  46313  subsaliuncl  46314  sge0rnn0  46324  sge00  46332  fsumlesge0  46333  sge0tsms  46336  sge0cl  46337  sge0f1o  46338  sge0fsum  46343  sge0supre  46345  sge0rnbnd  46349  sge0pnffigt  46352  sge0lefi  46354  sge0ltfirp  46356  sge0resplit  46362  sge0split  46365  sge0reuz  46403  sge0reuzb  46404  hoidmvlelem2  46552  smfpimcc  46764