| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > inteqi | Structured version Visualization version GIF version | ||
| Description: Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.) |
| Ref | Expression |
|---|---|
| inteqi.1 | ⊢ 𝐴 = 𝐵 |
| Ref | Expression |
|---|---|
| inteqi | ⊢ ∩ 𝐴 = ∩ 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inteqi.1 | . 2 ⊢ 𝐴 = 𝐵 | |
| 2 | inteq 4949 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ∩ 𝐴 = ∩ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∩ cint 4946 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ral 3062 df-rex 3071 df-int 4947 |
| This theorem is referenced by: elintrab 4960 ssintrab 4971 intmin2 4975 intsng 4983 intexrab 5347 intabs 5349 op1stb 5476 dfiin3g 5979 op2ndb 6247 ordintdif 6434 knatar 7377 uniordint 7821 oawordeulem 8592 oeeulem 8639 naddov3 8718 iinfi 9457 dfttrcl2 9764 tcsni 9783 rankval2 9858 rankval3b 9866 cf0 10291 cfval2 10300 cofsmo 10309 isf34lem4 10417 isf34lem7 10419 sstskm 10882 dfnn3 12280 trclun 15053 cycsubg 19226 efgval2 19742 00lsp 20979 alexsublem 24052 noextendlt 27714 nosepne 27725 nosepdm 27729 nosupbnd2lem1 27760 noinfbnd2lem1 27775 noetasuplem4 27781 bday0s 27873 intimafv 32720 dynkin 34168 imaiinfv 42704 elrfi 42705 onuniintrab 43238 naddov4 43396 naddwordnexlem4 43414 harval3 43551 relintab 43596 dfid7 43625 clcnvlem 43636 dfrtrcl5 43642 dfrcl2 43687 aiotajust 47096 dfaiota2 47098 ipolub0 48881 |
| Copyright terms: Public domain | W3C validator |