![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > inteq | Structured version Unicode version |
Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
inteq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq 3021 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | abbidv 2590 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | dfint2 4237 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | dfint2 4237 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ral 2803 df-int 4236 |
This theorem is referenced by: inteqi 4239 inteqd 4240 unissint 4259 uniintsn 4272 rint0 4275 intex 4555 intnex 4556 elreldm 5171 elxp5 6632 1stval2 6703 oev2 7072 fundmen 7492 xpsnen 7504 fiint 7698 elfir 7775 inelfi 7778 fiin 7782 cardmin2 8278 isfin2-2 8598 incexclem 13416 xpnnenOLD 13609 mreintcl 14651 ismred2 14659 fiinopn 18645 cmpfii 19143 ptbasfi 19285 fbssint 19542 shintcl 24884 chintcl 24886 rankeq1o 28352 neificl 28796 heibor1lem 28855 elrfi 29177 elrfirn 29178 |
Copyright terms: Public domain | W3C validator |