![]() |
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 4713 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∩ 𝐴 = ∩ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∩ cint 4710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-tru 1605 df-ex 1824 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-ral 3094 df-int 4711 |
This theorem is referenced by: elintrab 4722 ssintrab 4733 intmin2 4737 intsng 4745 intexrab 5057 intabs 5059 op1stb 5171 dfiin3g 5625 op2ndb 5874 ordintdif 6025 knatar 6879 uniordint 7284 oawordeulem 7918 oeeulem 7965 iinfi 8611 tcsni 8916 rankval2 8978 rankval3b 8986 cf0 9408 cfval2 9417 cofsmo 9426 isf34lem4 9534 isf34lem7 9536 sstskm 9999 dfnn3 11390 trclun 14162 cycsubg 18006 efgval2 18521 00lsp 19376 alexsublem 22256 dynkin 30842 noextendlt 32425 nosepne 32434 nosepdm 32437 nosupbnd2lem1 32464 noetalem3 32468 imaiinfv 38208 elrfi 38209 relintab 38838 dfid7 38868 clcnvlem 38879 dfrtrcl5 38885 dfrcl2 38915 aiotajust 42106 dfaiota2 42108 |
Copyright terms: Public domain | W3C validator |