![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq2i | Structured version Visualization version Unicode version |
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
ineq1i.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ineq2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | ineq2 3596 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-v 3015 df-in 3379 |
This theorem is referenced by: in4 3616 inindir 3618 indif2 3654 difun1 3671 dfrab3ss 3689 undif1 3810 difdifdir 3823 dfif3 3863 dfif5 3865 disjprsn 4003 intunsn 4244 rint0 4245 riin0 4322 csbres 5086 res0 5087 resres 5095 resundi 5096 resindi 5098 inres 5100 resiun2 5102 resopab 5129 dffr3 5179 dfse2 5180 dminxp 5255 imainrect 5256 resdmres 5305 dfpred2 5368 predidm 5381 funimacnv 5637 fresaun 5737 fresaunres2 5738 wfrlem13 7035 tfrlem10 7092 sbthlem5 7673 infssuni 7852 dfsup2 7945 en3lplem2 8107 wemapwe 8189 epfrs 8202 r0weon 8430 infxpenlem 8431 kmlem11 8577 ackbij1lem1 8637 ackbij1lem2 8638 axdc3lem4 8870 canthwelem 9062 dmaddpi 9302 dmmulpi 9303 ssxr 9690 dmhashres 12518 fz1isolem 12619 f1oun2prg 13010 fsumiun 13892 sadeq 14457 bitsres 14458 smuval2 14467 smumul 14478 ressinbas 15196 lubdm 16236 glbdm 16249 sylow2a 17282 lsmmod2 17337 lsmdisj2r 17346 ablfac1eu 17717 ressmplbas2 18690 opsrtoslem1 18718 pjdm 19281 rintopn 19950 ordtrest2 20231 cmpsublem 20425 kgentopon 20564 hausdiag 20671 uzrest 20923 ufprim 20935 trust 21255 metnrmlem3 21889 metnrmlem3OLD 21904 clsocv 22232 ismbl 22491 unmbl 22502 volinun 22511 voliunlem1 22515 ovolioo 22533 itg2cnlem2 22732 ellimc2 22844 limcflf 22848 lhop1lem 22977 lgsquadlem3 24296 rplogsum 24377 0pth 25312 1pthonlem2 25332 frgrancvvdeqlem4 25773 ex-in 25887 chdmj3i 27148 chdmj4i 27149 chjassi 27151 pjoml2i 27250 pjoml3i 27251 cmcmlem 27256 cmcm2i 27258 cmbr3i 27265 fh3i 27288 fh4i 27289 osumcor2i 27309 mayetes3i 27394 mdslmd3i 27997 mdexchi 28000 atabsi 28066 dmdbr5ati 28087 inin 28161 uniin2 28176 ordtrest2NEW 28736 hasheuni 28913 carsgclctunlem1 29155 eulerpartgbij 29211 fiblem 29237 cvmscld 30002 msrid 30189 dfpo2 30401 elrn3 30409 bj-inrab3 31534 poimirlem15 31957 mblfinlem2 31980 ftc1anclem6 32024 pol0N 33476 mapfzcons2 35563 diophrw 35603 conrel2d 36258 iunrelexp0 36296 hashnzfz 36670 disjinfi 37478 fourierdlem80 38107 sge0resplit 38307 sge0split 38310 caragenuncllem 38397 umgrislfupgrlem 39770 sPthisPth 39812 0pth-av 39893 1pthdlem2 39903 |
Copyright terms: Public domain | W3C validator |