![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldm2 | Structured version Visualization version GIF version |
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
eldm.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
eldm2 | ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldm.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | eldm2g 5898 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃wex 1774 ∈ wcel 2099 Vcvv 3462 〈cop 4629 dom cdm 5674 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-ss 3963 df-nul 4323 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-br 5146 df-dm 5684 |
This theorem is referenced by: dmss 5901 opeldm 5906 dmin 5910 dmiun 5912 dmuni 5913 dm0 5919 reldm0 5926 dmrnssfld 5969 dmcoss 5970 dmcosseq 5972 dmres 6013 iss 6036 dmsnopg 6216 relssdmrnOLD 6272 funssres 6595 dmfco 6990 fiun 7948 f1iun 7949 frrlem8 8300 frrlem10 8302 wfrlem12OLD 8342 axdc3lem2 10485 fnpr2ob 17568 gsum2d2 19968 cnlnssadj 32010 prsdm 33742 eldm3 35596 dfdm5 35609 iss2 38055 |
Copyright terms: Public domain | W3C validator |