Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrnmpt1s | Structured version Visualization version Unicode version |
Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.) |
Ref | Expression |
---|---|
rnmpt.1 | |
elrnmpt1s.1 |
Ref | Expression |
---|---|
elrnmpt1s |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2622 | . . 3 | |
2 | elrnmpt1s.1 | . . . . 5 | |
3 | 2 | eqeq2d 2632 | . . . 4 |
4 | 3 | rspcev 3309 | . . 3 |
5 | 1, 4 | mpan2 707 | . 2 |
6 | rnmpt.1 | . . . 4 | |
7 | 6 | elrnmpt 5372 | . . 3 |
8 | 7 | biimparc 504 | . 2 |
9 | 5, 8 | sylan 488 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wcel 1990 wrex 2913 cmpt 4729 crn 5115 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-mpt 4730 df-cnv 5122 df-dm 5124 df-rn 5125 |
This theorem is referenced by: wunex2 9560 dfod2 17981 dprd2dlem1 18440 dprd2da 18441 ordtbaslem 20992 subgntr 21910 opnsubg 21911 tgpconncomp 21916 tsmsxplem1 21956 xrge0gsumle 22636 xrge0tsms 22637 minveclem3b 23199 minveclem3 23200 minveclem4 23203 efsubm 24297 dchrisum0fno1 25200 xrge0tsmsd 29785 esumcvg 30148 esum2d 30155 msubco 31428 suprubrnmpt2 39467 infxrlbrnmpt2 39637 sge0xaddlem1 40650 |
Copyright terms: Public domain | W3C validator |