![]() |
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 2731 | . . 3 ⊢ 𝐶 = 𝐶 | |
2 | elrnmpt1s.1 | . . . 4 ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐶) | |
3 | 2 | rspceeqv 3633 | . . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 = 𝐶) → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
4 | 1, 3 | mpan2 688 | . 2 ⊢ (𝐷 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 𝐶 = 𝐵) |
5 | rnmpt.1 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
6 | 5 | elrnmpt 5955 | . . 3 ⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)) |
7 | 6 | biimparc 479 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝐶 = 𝐵 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
8 | 4, 7 | sylan 579 | 1 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2105 ∃wrex 3069 ↦ cmpt 5231 ran crn 5677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-mpt 5232 df-cnv 5684 df-dm 5686 df-rn 5687 |
This theorem is referenced by: wunex2 10737 dfod2 19474 dprd2dlem1 19953 dprd2da 19954 ordtbaslem 22913 subgntr 23832 opnsubg 23833 tgpconncomp 23838 tsmsxplem1 23878 xrge0gsumle 24570 xrge0tsms 24571 minveclem3b 25177 minveclem3 25178 minveclem4 25181 efsubm 26297 dchrisum0fno1 27251 fnpreimac 32164 xrge0tsmsd 32480 esumcvg 33383 esum2d 33390 msubco 34821 suprubrnmpt2 44255 infxrlbrnmpt2 44419 sge0xaddlem1 45448 |
Copyright terms: Public domain | W3C validator |