![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldm2 | Structured version Visualization version Unicode version |
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
eldm.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eldm2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldm.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eldm2g 5050 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 df-dm 4863 |
This theorem is referenced by: dmss 5053 opeldm 5057 dmin 5061 dmiun 5062 dmuni 5063 dm0 5067 reldm0 5071 dmrnssfld 5112 dmcoss 5113 dmcosseq 5115 dmres 5144 iss 5171 dmsnopg 5326 relssdmrn 5375 funssres 5641 dmfco 5962 fun11iun 6780 wfrlem12 7073 axdc3lem2 8907 gsum2d2 17655 cnlnssadj 27782 prsdm 28769 eldm3 30451 dfdm5 30467 frrlem11 30575 |
Copyright terms: Public domain | W3C validator |