Theorem rnmptssd 44492

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypotheses

Ref	Expression
rnmptssd.1	⊢ Ⅎ𝑥𝜑
rnmptssd.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
rnmptssd.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
rnmptssd	⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

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

Proof of Theorem rnmptssd

Step	Hyp	Ref	Expression
1		rnmptssd.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		rnmptssd.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
3	1, 2	ralrimia 3250	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
4		rnmptssd.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
5	4	rnmptss 7127	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
6	3, 5	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  Ⅎwnf 1778   ∈ wcel 2099  ∀wral 3056   ⊆ wss 3944   ↦ 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 2164  ax-ext 2698  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 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  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-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  infnsuprnmpt  44549  suprclrnmpt  44550  suprubrnmpt2  44551  suprubrnmpt  44552  fisupclrnmpt  44703  supxrleubrnmpt  44711  infxrlbrnmpt2  44715  supxrrernmpt  44726  suprleubrnmpt  44727  infrnmptle  44728  infxrunb3rnmpt  44733  supxrre3rnmpt  44734  supminfrnmpt  44750  infxrrnmptcl  44752  infxrgelbrnmpt  44759  infrpgernmpt  44770  supminfxrrnmpt  44776  liminfcl  45074  fourierdlem31  45449  fourierdlem53  45470  sge0xaddlem2  45745  sge0reuz  45758  sge0reuzb  45759  meadjiun  45777  hoidmvlelem2  45907  iunhoiioolem  45986  vonioolem1  45991  smflimsuplem4  46134