Theorem elrnmptd 5941

Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
elrnmptd.f	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
elrnmptd.x	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
elrnmptd.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
elrnmptd	⊢ (𝜑 → 𝐶 ∈ ran 𝐹)

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmptd

Step	Hyp	Ref	Expression
1		elrnmptd.x	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
2		elrnmptd.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		elrnmptd.f	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	elrnmpt 5936	. . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
5	2, 4	syl 18	. 2 ⊢ (𝜑 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
6	1, 5	mpbird 260	1 ⊢ (𝜑 → 𝐶 ∈ ran 𝐹)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086   ↦ cmpt 5185  ran crn 5648

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-pr 5390

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is used by:  pwfilem  9287  evls1maprnss  22657  elrgspnlem1  33736  elrgspnlem2  33737  elrgspnlem3  33738  nsgmgc  33896  nsgqusf1olem1  33897  algextdeglem4  34285  zarclsun  34435  rnmptssrn  46118  infnsuprnmpt  46183  supminfrnmpt  46377  supminfxrrnmpt  46403  sge0sup  47323  sge0resplit  47338  sge0xaddlem2  47366  sge0pnfmpt  47377  sge0reuz  47379  sge0reuzb  47380  hoidmvlelem2  47528