![]() |
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 4700 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∩ 𝐴 = ∩ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ∩ cint 4697 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-int 4698 |
This theorem is referenced by: elintrab 4709 ssintrab 4720 intmin2 4724 intsng 4732 intexrab 5045 intabs 5047 op1stb 5160 dfiin3g 5612 op2ndb 5861 ordintdif 6012 knatar 6862 uniordint 7267 oawordeulem 7901 oeeulem 7948 iinfi 8592 tcsni 8896 rankval2 8958 rankval3b 8966 cf0 9388 cfval2 9397 cofsmo 9406 isf34lem4 9514 isf34lem7 9516 sstskm 9979 dfnn3 11366 trclun 14132 cycsubg 17973 efgval2 18488 00lsp 19340 alexsublem 22218 dynkin 30764 noextendlt 32350 nosepne 32359 nosepdm 32362 nosupbnd2lem1 32389 noetalem3 32393 imaiinfv 38093 elrfi 38094 relintab 38723 dfid7 38753 clcnvlem 38764 dfrtrcl5 38770 dfrcl2 38800 aiotajust 41974 dfaiota2 41976 |
Copyright terms: Public domain | W3C validator |