Theorem elrnmpt 5948

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∃wrex 3089   ↦ cmpt 5192  ran crn 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is used by:  elrnmpt1s  5949  elrnmptd  5953  elrnmptdv  5955  elrnmpt2d  5956  nelrnmpt  5957  elimampt  6045  onnseq  8327  oarec  8543  fifo  9388  infpwfien  10051  fin23lem38  10337  fin1a2lem13  10400  ac6num  10467  isercoll2  15725  iserodd  16899  gsumwspan  18909  odf1o2  19647  mplcoe5lem  22199  neitr  23346  ordtbas2  23357  ordtopn1  23360  ordtopn2  23361  pnfnei  23386  mnfnei  23387  pnrmcld  23508  2ndcomap  23624  dis2ndc  23626  ptpjopn  23778  fbasrn  24050  elfm  24113  rnelfmlem  24118  rnelfm  24119  fmfnfmlem3  24122  fmfnfmlem4  24123  fmfnfm  24124  ptcmplem2  24219  tsmsfbas  24294  ustuqtoplem  24405  utopsnneiplem  24413  utopsnnei  24415  utopreg  24418  fmucnd  24457  neipcfilu  24461  imasdsf1olem  24539  xpsdsval  24547  met1stc  24687  metustel  24716  metustsym  24721  metuel2  24731  metustbl  24732  restmetu  24736  xrtgioo  24973  minveclem3b  25596  uniioombllem3  25753  dvivth  26178  gausslemma2dlem1a  27538  acunirnmpt  33013  acunirnmpt2  33014  acunirnmpt2f  33015  fnpreimac  33024  trsp2cyc  33452  elrgspnlem1  33571  elrgspnlem2  33572  elrgspn  33575  nsgqusf1olem2  33732  nsgqusf1olem3  33733  locfinreflem  34239  zarclsint  34271  zarcls  34273  ordtconnlem1  34323  esumcst  34462  esumrnmpt2  34467  measdivcstALTV  34624  oms0  34696  omssubadd  34699  cvmsss2  35774  poimirlem16  38315  poimirlem19  38318  poimirlem24  38323  poimirlem27  38326  itg2addnclem2  38351  suprnmpt  45920  rnmptpr  45923  wessf1ornlem  45931  disjrnmpt2  45934  disjf1o  45937  disjinfi  45938  choicefi  45945  rnmptlb  45986  rnmptbddlem  45987  rnmptbd2lem  45991  infnsuprnmpt  45993  elmptima  46001  supxrleubrnmpt  46148  suprleubrnmpt  46164  infrnmptle  46165  infxrunb3rnmpt  46170  supminfrnmpt  46187  infxrgelbrnmpt  46196  infrpgernmpt  46207  supminfxrrnmpt  46213  stoweidlem27  46769  stoweidlem31  46773  stoweidlem35  46777  stirlinglem5  46820  stirlinglem13  46828  fourierdlem80  46928  fourierdlem93  46941  fourierdlem103  46951  fourierdlem104  46952  subsaliuncllem  47099  subsaliuncl  47100  sge0rnn0  47110  sge00  47118  fsumlesge0  47119  sge0tsms  47122  sge0cl  47123  sge0f1o  47124  sge0fsum  47129  sge0supre  47131  sge0rnbnd  47135  sge0pnffigt  47138  sge0lefi  47140  sge0ltfirp  47142  sge0resplit  47148  sge0split  47151  sge0reuz  47189  sge0reuzb  47190  hoidmvlelem2  47338  smfpimcc  47550