![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrnmpt1s | Structured version Visualization version GIF version |
Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
Ref | Expression |
---|---|
rnmpt.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
elrnmpt1s.1 | ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
elrnmpt1s | ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2799 | . . 3 ⊢ 𝐶 = 𝐶 | |
2 | elrnmpt1s.1 | . . . 4 ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) | |
3 | 2 | rspceeqv 3515 | . . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 = 𝐶) → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
4 | 1, 3 | mpan2 683 | . 2 ⊢ (𝐷 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
5 | rnmpt.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | elrnmpt 5576 | . . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) |
7 | 6 | biimparc 472 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝐶 = 𝐵 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
8 | 4, 7 | sylan 576 | 1 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∃wrex 3090 ↦ cmpt 4922 ran crn 5313 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-br 4844 df-opab 4906 df-mpt 4923 df-cnv 5320 df-dm 5322 df-rn 5323 |
This theorem is referenced by: wunex2 9848 dfod2 18294 dprd2dlem1 18756 dprd2da 18757 ordtbaslem 21321 subgntr 22238 opnsubg 22239 tgpconncomp 22244 tsmsxplem1 22284 xrge0gsumle 22964 xrge0tsms 22965 minveclem3b 23538 minveclem3 23539 minveclem4 23542 efsubm 24639 dchrisum0fno1 25552 xrge0tsmsd 30301 esumcvg 30664 esum2d 30671 msubco 31945 suprubrnmpt2 40214 infxrlbrnmpt2 40380 sge0xaddlem1 41393 |
Copyright terms: Public domain | W3C validator |