Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dmeq | Structured version Visualization version GIF version |
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
dmeq | ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmss 5765 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵) | |
2 | dmss 5765 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴) | |
3 | 1, 2 | anim12i 614 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴)) |
4 | eqss 3981 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3981 | . 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴)) | |
6 | 3, 4, 5 | 3imtr4i 294 | 1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1533 ⊆ wss 3935 dom cdm 5549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-br 5059 df-dm 5559 |
This theorem is referenced by: dmeqi 5767 dmeqd 5768 xpid11 5796 resresdm 6084 fneq1 6438 eqfnfv2 6797 funopdmsn 6906 nvof1o 7031 offval 7410 ofrfval 7411 offval3 7677 suppval 7826 smoeq 7981 tz7.44lem1 8035 tz7.44-2 8037 tz7.44-3 8038 ereq1 8290 fundmeng 8578 fseqenlem2 9445 dfac3 9541 dfac9 9556 dfac12lem1 9563 dfac12r 9566 ackbij2lem2 9656 ackbij2lem3 9657 r1om 9660 cfsmolem 9686 cfsmo 9687 dcomex 9863 axdc2lem 9864 axdc3lem2 9867 axdc3lem4 9869 ac7g 9890 ttukey2g 9932 fundmge2nop0 13844 s4dom 14275 relexp0g 14375 relexpsucnnr 14378 dfrtrcl2 14415 ello1 14866 elo1 14877 bpolylem 15396 bpolyval 15397 isoval 17029 istsr 17821 islindf 20950 decpmatval0 21366 pmatcollpw3lem 21385 ordtval 21791 dfac14 22220 fmval 22545 fmf 22547 blfvalps 22987 tmsval 23085 cfilfval 23861 caufval 23872 isibl 24360 elcpn 24525 iscgrg 26292 uhgr0e 26850 incistruhgr 26858 ausgrusgri 26947 egrsubgr 27053 vtxdgfval 27243 vtxdg0e 27250 1egrvtxdg1 27285 eupth0 27987 ex-dm 28212 eldmne0 30367 f1ocnt 30519 tocycfv 30746 tocycf 30754 tocyc01 30755 cycpmco2f1 30761 cycpmco2rn 30762 cycpmco2lem1 30763 cycpmco2lem2 30764 cycpmco2lem3 30765 cycpmco2lem4 30766 cycpmco2lem5 30767 cycpmco2lem6 30768 cycpmco2lem7 30769 cycpmco2 30770 cycpm3cl2 30773 cycpmconjv 30779 tocyccntz 30781 cyc3evpm 30787 cycpmgcl 30790 cycpmconjslem2 30792 cyc3conja 30794 locfinreflem 31099 pstmval 31130 cntnevol 31482 omsval 31546 sitgval 31585 elprob 31662 cndprobval 31686 rrvmbfm 31695 bnj1385 32099 bnj1400 32102 bnj1014 32228 bnj1015 32229 bnj1326 32293 bnj1321 32294 bnj1491 32324 mrsubfval 32750 rdgprc0 33033 dfrdg2 33035 bdayval 33150 bdayfo 33177 noprefixmo 33197 nosupdm 33199 nosupfv 33201 nosupres 33202 nosupbnd1lem1 33203 nosupbnd1lem3 33205 nosupbnd1lem5 33207 nosupbnd2 33211 noetalem3 33214 brdomaing 33391 fwddifval 33618 fwddifnval 33619 filnetlem4 33724 cureq 34862 ismtyval 35072 isass 35118 isexid 35119 ismgmOLD 35122 elrefrels2 35751 elrefrels3 35752 refreleq 35754 elcnvrefrels2 35764 elcnvrefrels3 35765 elrefsymrels2 35799 eleqvrels2 35821 eleqvrels3 35822 dmqseq 35869 aomclem6 39652 aomclem8 39654 dfac21 39659 rclexi 39968 rtrclex 39970 rtrclexi 39974 cnvrcl0 39978 dfrtrcl5 39982 dfrcl2 40012 gneispace2 40475 ssnnf1octb 41449 sge0val 42642 ismea 42727 caragenval 42769 isome 42770 issmflem 42998 isomgreqve 43984 fnxpdmdm 44029 elbigo 44605 |
Copyright terms: Public domain | W3C validator |