![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq12 | Structured version Visualization version Unicode version |
Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.) |
Ref | Expression |
---|---|
ineq12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 3629 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ineq2 3630 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan9eq 2507 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 df-in 3413 |
This theorem is referenced by: ineq12i 3634 ineq12d 3637 ineqan12d 3638 fnun 5687 undifixp 7563 endisj 7664 sbthlem8 7694 fiin 7941 pm54.43 8439 kmlem9 8593 indistopon 20028 epttop 20036 restbas 20186 ordtbas2 20219 txbas 20594 ptbasin 20604 trfbas2 20870 snfil 20891 fbasrn 20911 trfil2 20914 fmfnfmlem3 20983 ustuqtop2 21269 minveclem3b 22382 minveclem3bOLD 22394 isperp 24769 frrlem4 30529 diophin 35627 kelac2lem 35934 |
Copyright terms: Public domain | W3C validator |