Theorem elrnmpt1s 5803

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)

Hypotheses

Ref	Expression
rnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
elrnmpt1s.1	⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)

Assertion

Ref	Expression
elrnmpt1s	⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)

Distinct variable groups:   𝑥,𝐶   𝑥,𝐴   𝑥,𝐷

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

Proof of Theorem elrnmpt1s

Step	Hyp	Ref	Expression
1		eqid 2758	. . 3 ⊢ 𝐶 = 𝐶
2		elrnmpt1s.1	. . . 4 ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶)
3	2	rspceeqv 3558	. . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 = 𝐶) → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
4	1, 3	mpan2 690	. 2 ⊢ (𝐷 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)
5		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
6	5	elrnmpt 5802	. . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
7	6	biimparc 483	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝐶 = 𝐵 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)
8	4, 7	sylan 583	1 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071   ↦ cmpt 5116  ran crn 5529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-mpt 5117  df-cnv 5536  df-dm 5538  df-rn 5539

This theorem is referenced by:  wunex2  10211  dfod2  18772  dprd2dlem1  19245  dprd2da  19246  ordtbaslem  21902  subgntr  22821  opnsubg  22822  tgpconncomp  22827  tsmsxplem1  22867  xrge0gsumle  23548  xrge0tsms  23549  minveclem3b  24142  minveclem3  24143  minveclem4  24146  efsubm  25256  dchrisum0fno1  26208  fnpreimac  30545  xrge0tsmsd  30856  esumcvg  31586  esum2d  31593  msubco  33022  suprubrnmpt2  42303  infxrlbrnmpt2  42458  sge0xaddlem1  43483