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 3436 | . . . . 5 ⊢ 𝑦 ∈ V | |
2 | vex 3436 | . . . . 5 ⊢ 𝑥 ∈ V | |
3 | 1, 2 | brcnv 5791 | . . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) |
4 | 3 | exbii 1850 | . . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦) |
5 | 4 | abbii 2808 | . 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} |
6 | dfrn2 5797 | . 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} | |
7 | df-dm 5599 | . 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | |
8 | 5, 6, 7 | 3eqtr4ri 2777 | 1 ⊢ dom 𝐴 = ran ◡𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∃wex 1782 {cab 2715 class class class wbr 5074 ◡ccnv 5588 dom cdm 5589 ran crn 5590 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-cnv 5597 df-dm 5599 df-rn 5600 |
This theorem is referenced by: dmcnvcnv 5842 rncnvcnv 5843 rncoeq 5884 cnvimass 5989 cnvimarndm 5990 dminxp 6083 cnvsn0 6113 rnsnopg 6124 dmmpt 6143 dmco 6158 cores2 6163 cnvssrndm 6174 unidmrn 6182 dfdm2 6184 funimacnv 6515 foimacnv 6733 funcocnv2 6741 fimacnvOLD 6948 f1opw2 7524 cnvexg 7771 tz7.48-3 8275 fopwdom 8867 sbthlem4 8873 fodomr 8915 cnvfi 8963 f1opwfi 9123 zorn2lem4 10255 trclublem 14706 relexpcnv 14746 unbenlem 16609 gsumpropd2lem 18363 pjdm 20914 paste 22445 hmeores 22922 icchmeo 24104 fcnvgreu 31010 ffsrn 31064 gsummpt2co 31308 tocycfvres1 31377 tocycfvres2 31378 cycpmfvlem 31379 cycpmfv3 31382 coinfliprv 32449 itg2addnclem2 35829 rncnv 36436 lnmlmic 40913 dmnonrel 41198 cnvrcl0 41233 conrel1d 41271 |
Copyright terms: Public domain | W3C validator |