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 4882 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∩ 𝐴 = ∩ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∩ cint 4879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-ral 3069 df-int 4880 |
This theorem is referenced by: elintrab 4891 ssintrab 4902 intmin2 4906 intsng 4916 intexrab 5264 intabs 5266 op1stb 5386 dfiin3g 5874 op2ndb 6130 ordintdif 6315 knatar 7228 uniordint 7651 oawordeulem 8385 oeeulem 8432 iinfi 9176 dfttrcl2 9482 tcsni 9501 rankval2 9576 rankval3b 9584 cf0 10007 cfval2 10016 cofsmo 10025 isf34lem4 10133 isf34lem7 10135 sstskm 10598 dfnn3 11987 trclun 14725 cycsubg 18827 efgval2 19330 00lsp 20243 alexsublem 23195 intimafv 31043 dynkin 32135 noextendlt 33872 nosepne 33883 nosepdm 33887 nosupbnd2lem1 33918 noinfbnd2lem1 33933 noetasuplem4 33939 bday0s 34022 imaiinfv 40515 elrfi 40516 harval3 41145 relintab 41191 dfid7 41220 clcnvlem 41231 dfrtrcl5 41237 dfrcl2 41282 aiotajust 44576 dfaiota2 44578 ipolub0 46278 |
Copyright terms: Public domain | W3C validator |