![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq2 | Structured version Visualization version Unicode version |
Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
ineq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 3638 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | incom 3636 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | incom 3636 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3eqtr4g 2520 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 |
This theorem is referenced by: ineq12 3640 ineq2i 3642 ineq2d 3645 uneqin 3705 intprg 4282 wefrc 4846 onfr 5480 onnseq 7088 qsdisj 7465 disjenex 7755 fiint 7873 elfiun 7969 dffi3 7970 cplem2 8386 dfac5 8584 kmlem2 8606 kmlem13 8617 kmlem14 8618 ackbij1lem16 8690 fin23lem12 8786 fin23lem19 8791 fin23lem33 8800 uzin2 13455 pgpfac1lem3 17758 pgpfac1lem5 17760 pgpfac1 17761 inopn 19977 basis1 20013 basis2 20014 baspartn 20017 fctop 20067 cctop 20069 ordtbaslem 20252 hausnei2 20417 cnhaus 20418 nrmsep 20421 isnrm2 20422 dishaus 20446 ordthauslem 20447 dfcon2 20482 nconsubb 20486 finlocfin 20583 dissnlocfin 20592 locfindis 20593 kgeni 20600 pthaus 20701 txhaus 20710 xkohaus 20716 regr1lem 20802 fbasssin 20899 fbun 20903 fbunfip 20932 filcon 20946 isufil2 20971 ufileu 20982 filufint 20983 fmfnfmlem4 21020 fmfnfm 21021 fclsopni 21078 fclsbas 21084 fclsrest 21087 isfcf 21097 tsmsfbas 21190 ustincl 21270 ust0 21282 metreslem 21425 methaus 21583 qtopbaslem 21827 metnrmlem3 21926 metnrmlem3OLD 21941 ismbl 22528 shincl 27082 chincl 27200 chdmm1 27226 ledi 27241 cmbr 27285 cmbr3i 27301 cmbr3 27309 pjoml2 27312 stcltrlem1 27977 mdbr 27995 dmdbr 28000 cvmd 28037 cvexch 28075 sumdmdii 28116 mddmdin0i 28132 ofpreima2 28317 crefeq 28720 ldgenpisyslem1 29033 ldgenpisys 29036 inelsros 29048 diffiunisros 29049 elcarsg 29185 carsgclctunlem2 29199 carsgclctun 29201 ballotlemfval 29370 ballotlemgval 29404 ballotlemgvalOLD 29442 cvmscbv 30029 cvmsdisj 30041 cvmsss2 30045 nepss 30398 tailfb 31081 mblfinlem2 32022 lshpinN 32599 elrfi 35580 fipjust 36213 conrel1d 36299 csbresgVD 37331 disjf1 37494 qinioo 37674 fouriersw 38132 nnfoctbdjlem 38330 meadjun 38337 caragenel 38353 |
Copyright terms: Public domain | W3C validator |