![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inteq | Structured version Visualization version Unicode version |
Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
inteq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq 2999 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | abbidv 2580 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfint2 4250 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfint2 4250 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2521 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ral 2754 df-int 4249 |
This theorem is referenced by: inteqi 4252 inteqd 4253 unissint 4273 uniintsn 4286 rint0 4289 intex 4576 intnex 4577 elreldm 5081 elxp5 6770 1stval2 6842 oev2 7256 fundmen 7674 xpsnen 7687 fiint 7879 elfir 7960 inelfi 7963 fiin 7967 cardmin2 8463 isfin2-2 8780 incexclem 13949 mreintcl 15556 ismred2 15564 fiinopn 19986 cmpfii 20479 ptbasfi 20651 fbssint 20908 shintcl 27039 chintcl 27041 inelpisys 29027 rankeq1o 30988 neificl 32128 heibor1lem 32187 elrfi 35582 elrfirn 35583 |
Copyright terms: Public domain | W3C validator |