Theorem elrnmptd 5957

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 5952	. . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
5	2, 4	syl 17	. 2 ⊢ (𝜑 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
6	1, 5	mpbird 257	1 ⊢ (𝜑 → 𝐶 ∈ ran 𝐹)

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099  ∃wrex 3066   ↦ cmpt 5225  ran crn 5673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-rex 3067  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-mpt 5226  df-cnv 5680  df-dm 5682  df-rn 5683

This theorem is referenced by:  pwfilem  9195  nsgmgc  33116  nsgqusf1olem1  33117  evls1maprnss  33365  algextdeglem4  33382  zarclsun  33465  rnmptssrn  44549  infnsuprnmpt  44620  supminfrnmpt  44821  supminfxrrnmpt  44847  sge0sup  45773  sge0resplit  45788  sge0xaddlem2  45816  sge0pnfmpt  45827  sge0reuz  45829  sge0reuzb  45830  hoidmvlelem2  45978

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »