Theorem elrnmpt 5968

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∃wrex 3069   ↦ cmpt 5224  ran crn 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-mpt 5225  df-cnv 5692  df-dm 5694  df-rn 5695

This theorem is referenced by:  elrnmpt1s  5969  elrnmptd  5973  elrnmptdv  5975  elrnmpt2d  5976  elimampt  6060  onnseq  8385  oarec  8601  fifo  9473  infpwfien  10103  fin23lem38  10390  fin1a2lem13  10453  ac6num  10520  isercoll2  15706  iserodd  16874  gsumwspan  18860  odf1o2  19592  mplcoe5lem  22058  neitr  23189  ordtbas2  23200  ordtopn1  23203  ordtopn2  23204  pnfnei  23229  mnfnei  23230  pnrmcld  23351  2ndcomap  23467  dis2ndc  23469  ptpjopn  23621  fbasrn  23893  elfm  23956  rnelfmlem  23961  rnelfm  23962  fmfnfmlem3  23965  fmfnfmlem4  23966  fmfnfm  23967  ptcmplem2  24062  tsmsfbas  24137  ustuqtoplem  24249  utopsnneiplem  24257  utopsnnei  24259  utopreg  24262  fmucnd  24302  neipcfilu  24306  imasdsf1olem  24384  xpsdsval  24392  met1stc  24535  metustel  24564  metustsym  24569  metuel2  24579  metustbl  24580  restmetu  24584  xrtgioo  24829  minveclem3b  25463  uniioombllem3  25621  dvivth  26050  gausslemma2dlem1a  27410  acunirnmpt  32670  acunirnmpt2  32671  acunirnmpt2f  32672  fnpreimac  32682  trsp2cyc  33144  elrgspnlem1  33247  elrgspnlem2  33248  elrgspn  33251  nsgqusf1olem2  33443  nsgqusf1olem3  33444  locfinreflem  33840  zarclsint  33872  zarcls  33874  ordtconnlem1  33924  esumcst  34065  esumrnmpt2  34070  measdivcstALTV  34227  oms0  34300  omssubadd  34303  cvmsss2  35280  poimirlem16  37644  poimirlem19  37647  poimirlem24  37652  poimirlem27  37655  itg2addnclem2  37680  nelrnmpt  45094  suprnmpt  45184  rnmptpr  45187  wessf1ornlem  45195  disjrnmpt2  45198  disjf1o  45201  disjinfi  45202  choicefi  45210  rnmptlb  45255  rnmptbddlem  45256  rnmptbd2lem  45260  infnsuprnmpt  45262  elmptima  45270  supxrleubrnmpt  45422  suprleubrnmpt  45438  infrnmptle  45439  infxrunb3rnmpt  45444  supminfrnmpt  45461  infxrgelbrnmpt  45470  infrpgernmpt  45481  supminfxrrnmpt  45487  stoweidlem27  46047  stoweidlem31  46051  stoweidlem35  46055  stirlinglem5  46098  stirlinglem13  46106  fourierdlem80  46206  fourierdlem93  46219  fourierdlem103  46229  fourierdlem104  46230  subsaliuncllem  46377  subsaliuncl  46378  sge0rnn0  46388  sge00  46396  fsumlesge0  46397  sge0tsms  46400  sge0cl  46401  sge0f1o  46402  sge0fsum  46407  sge0supre  46409  sge0rnbnd  46413  sge0pnffigt  46416  sge0lefi  46418  sge0ltfirp  46420  sge0resplit  46426  sge0split  46429  sge0reuz  46467  sge0reuzb  46468  hoidmvlelem2  46616  smfpimcc  46828