Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfdm4 | Structured version Visualization version GIF version |
Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996.) |
Ref | Expression |
---|---|
dfdm4 | ⊢ dom 𝐴 = ran ◡𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3402 | . . . . 5 ⊢ 𝑦 ∈ V | |
2 | vex 3402 | . . . . 5 ⊢ 𝑥 ∈ V | |
3 | 1, 2 | brcnv 5725 | . . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) |
4 | 3 | exbii 1854 | . . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦) |
5 | 4 | abbii 2803 | . 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} |
6 | dfrn2 5731 | . 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} | |
7 | df-dm 5535 | . 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
8 | 5, 6, 7 | 3eqtr4ri 2772 | 1 ⊢ dom 𝐴 = ran ◡𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∃wex 1786 {cab 2716 class class class wbr 5030 ◡ccnv 5524 dom cdm 5525 ran crn 5526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-dif 3846 df-un 3848 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-br 5031 df-opab 5093 df-cnv 5533 df-dm 5535 df-rn 5536 |
This theorem is referenced by: dmcnvcnv 5776 rncnvcnv 5777 rncoeq 5818 cnvimass 5923 cnvimarndm 5924 dminxp 6012 cnvsn0 6042 rnsnopg 6053 dmmpt 6072 dmco 6087 cores2 6092 cnvssrndm 6103 unidmrn 6111 dfdm2 6113 funimacnv 6420 foimacnv 6635 funcocnv2 6642 fimacnvOLD 6848 f1opw2 7416 cnvexg 7655 tz7.48-3 8109 fopwdom 8674 sbthlem4 8680 fodomr 8718 cnvfi 8777 f1opwfi 8901 zorn2lem4 9999 trclublem 14444 relexpcnv 14484 unbenlem 16344 gsumpropd2lem 18005 pjdm 20523 paste 22045 hmeores 22522 icchmeo 23693 fcnvgreu 30585 ffsrn 30639 gsummpt2co 30885 tocycfvres1 30954 tocycfvres2 30955 cycpmfvlem 30956 cycpmfv3 30959 coinfliprv 32019 itg2addnclem2 35452 rncnv 36059 lnmlmic 40485 dmnonrel 40743 cnvrcl0 40778 conrel1d 40817 |
Copyright terms: Public domain | W3C validator |