![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmeq | Structured version Visualization version Unicode version |
Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.) |
Ref | Expression |
---|---|
dmeq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmss 5034 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dmss 5034 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anim12i 570 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eqss 3447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqss 3447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3imtr4i 270 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-dm 4844 |
This theorem is referenced by: dmeqi 5036 dmeqd 5037 xpid11 5056 fneq1 5664 eqfnfv2 5977 nvof1o 6179 offval 6538 ofrfval 6539 offval3 6787 suppval 6916 smoeq 7069 tz7.44lem1 7123 tz7.44-2 7125 tz7.44-3 7126 ereq1 7370 fundmeng 7644 fseqenlem2 8456 dfac3 8552 dfac9 8566 dfac12lem1 8573 dfac12r 8576 ackbij2lem2 8670 ackbij2lem3 8671 r1om 8674 cfsmolem 8700 cfsmo 8701 dcomex 8877 axdc2lem 8878 axdc3lem2 8881 axdc3lem4 8883 ac7g 8904 ttukey2g 8946 s4dom 13004 relexp0g 13085 relexpsucnnr 13088 dfrtrcl2 13125 ello1 13579 elo1 13590 bpolylem 14101 bpolyval 14102 isoval 15670 istsr 16463 islindf 19370 decpmatval0 19788 pmatcollpw3lem 19807 ordtval 20205 dfac14 20633 fmval 20958 fmf 20960 blfvalps 21398 tmsval 21496 cfilfval 22234 caufval 22245 isibl 22723 elcpn 22888 iscgrg 24557 isuhgra 25025 uhgrac 25032 uhgraeq12d 25034 isuslgra 25070 isusgra 25071 usgraeq12d 25089 wlks 25247 wlkcompim 25254 wlkelwrd 25258 ex-dm 25889 isass 26044 isexid 26045 ismgmOLD 26048 f1ocnt 28376 locfinreflem 28667 pstmval 28698 cntnevol 29050 omsval 29117 omsvalOLD 29121 sitgval 29165 elprob 29242 cndprobval 29266 rrvmbfm 29275 bnj1385 29644 bnj1400 29647 bnj1014 29771 bnj1015 29772 bnj1326 29835 bnj1321 29836 bnj1491 29866 mrsubfval 30146 rdgprc0 30440 dfrdg2 30442 frrlem5e 30522 bdayval 30535 bdayfo 30564 nofulllem5 30595 brdomaing 30702 fwddifval 30929 fwddifnval 30930 filnetlem4 31037 ismtyval 32132 aomclem6 35917 aomclem8 35919 dfac21 35924 rclexi 36222 rtrclex 36224 rtrclexi 36228 cnvrcl0 36232 dfrtrcl5 36236 dfrcl2 36266 ssnnf1octb 37470 sge0val 38208 ismea 38289 caragenval 38314 isome 38315 resresdm 39010 fundmge2nop 39026 structvtxvallem 39122 uhgr0e 39164 incistruhgr 39171 ausgrusgri 39255 egrsubgr 39349 vtxdgfval 39528 vtxdg0e 39534 uhg0e 39741 uhgres 39744 isfusgra 39789 fnxpdmdm 39821 offval0 40356 elbigo 40415 |
Copyright terms: Public domain | W3C validator |