Theorem elrnmpt 5945

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2146  ∃wrex 3090   ↦ cmpt 5189  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  elrnmpt1s  5946  elrnmptd  5950  elrnmptdv  5952  elrnmpt2d  5953  nelrnmpt  5954  elimampt  6041  onnseq  8366  oarec  8584  fifo  9437  infpwfien  10154  fin23lem38  10440  fin1a2lem13  10503  ac6num  10570  isercoll2  15851  iserodd  17028  gsumwspan  19057  odf1o2  19802  mplcoe5lem  22363  neitr  23513  ordtbas2  23524  ordtopn1  23527  ordtopn2  23528  pnfnei  23553  mnfnei  23554  pnrmcld  23675  2ndcomap  23792  dis2ndc  23794  ptpjopn  23946  fbasrn  24218  elfm  24281  rnelfmlem  24286  rnelfm  24287  fmfnfmlem3  24290  fmfnfmlem4  24291  fmfnfm  24292  ptcmplem2  24387  tsmsfbas  24462  ustuqtoplem  24573  utopsnneiplem  24581  utopsnnei  24583  utopreg  24586  fmucnd  24625  neipcfilu  24629  imasdsf1olem  24707  xpsdsval  24715  met1stc  24855  metustel  24884  metustsym  24889  metuel2  24899  metustbl  24900  restmetu  24904  xrtgioo  25141  minveclem3b  25764  uniioombllem3  25921  dvivth  26345  gausslemma2dlem1a  27707  acunirnmpt  33310  fnpreimac  33321  trsp2cyc  33740  elrgspnlem1  33859  elrgspnlem2  33860  elrgspn  33863  nsgqusf1olem2  34021  nsgqusf1olem3  34022  locfinreflem  34528  zarclsint  34560  zarcls  34562  ordtconnlem1  34612  esumcst  34751  esumrnmpt2  34756  measdivcstALTV  34914  oms0  34985  omssubadd  34988  cvmsss2  36163  poimirlem16  38700  poimirlem19  38703  poimirlem24  38708  poimirlem27  38711  itg2addnclem2  38736  suprnmpt  46334  rnmptpr  46337  wessf1ornlem  46345  disjrnmpt2  46348  disjf1o  46351  disjinfi  46352  choicefi  46359  rnmptlb  46400  rnmptbddlem  46401  rnmptbd2lem  46405  infnsuprnmpt  46407  elmptima  46415  supxrleubrnmpt  46561  suprleubrnmpt  46577  infrnmptle  46578  infxrunb3rnmpt  46583  supminfrnmpt  46600  infxrgelbrnmpt  46609  infrpgernmpt  46620  supminfxrrnmpt  46626  stoweidlem27  47182  stoweidlem31  47186  stoweidlem35  47190  stirlinglem5  47233  stirlinglem13  47241  fourierdlem80  47341  fourierdlem93  47354  fourierdlem103  47364  fourierdlem104  47365  subsaliuncllem  47512  subsaliuncl  47513  sge0rnn0  47523  sge00  47531  fsumlesge0  47532  sge0tsms  47535  sge0cl  47536  sge0f1o  47537  sge0fsum  47542  sge0supre  47544  sge0rnbnd  47548  sge0pnffigt  47551  sge0lefi  47553  sge0ltfirp  47555  sge0resplit  47561  sge0split  47564  sge0reuz  47602  sge0reuzb  47603  hoidmvlelem2  47751  smfpimcc  47963