![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eldm2 | 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 4835 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∃wex 1502 ∈ wcel 2158 Vcvv 2749 〈cop 3607 dom cdm 4638 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-un 3145 df-sn 3610 df-pr 3611 df-op 3613 df-br 4016 df-dm 4648 |
This theorem is referenced by: dmss 4838 opeldm 4842 dmin 4847 dmiun 4848 dmuni 4849 dm0 4853 reldm0 4857 dmrnssfld 4902 dmcoss 4908 dmcosseq 4910 dmres 4940 iss 4965 dmxpss 5071 dmsnopg 5112 relssdmrn 5161 funssres 5270 fun11iun 5494 tfrlemibxssdm 6341 tfr1onlembxssdm 6357 tfrcllembxssdm 6370 fnpr2ob 12777 |
Copyright terms: Public domain | W3C validator |