![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inteqd | Structured version Visualization version GIF version |
Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.) |
Ref | Expression |
---|---|
inteqd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
inteqd | ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inteqd.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | inteq 4952 | . 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∩ cint 4949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-ral 3059 df-rex 3068 df-int 4950 |
This theorem is referenced by: intprgOLD 4987 elreldm 5937 ordintdif 6419 fniinfv 6976 onsucmin 7824 elxp5 7931 1stval2 8010 2ndval2 8011 naddcllem 8696 naddov2 8699 naddcom 8702 naddrid 8703 naddasslem1 8714 naddasslem2 8715 naddass 8716 fundmen 9055 xpsnen 9079 unblem2 9320 unblem3 9321 fiint 9348 elfi2 9437 fi0 9443 elfiun 9453 tcvalg 9761 tz9.12lem3 9812 rankvalb 9820 rankvalg 9840 ranksnb 9850 rankonidlem 9851 cardval3 9975 cardidm 9982 harsucnn 10021 cfval 10270 cflim3 10285 coftr 10296 isfin3ds 10352 fin23lem17 10361 fin23lem39 10373 isf33lem 10389 isf34lem5 10401 isf34lem6 10403 wuncval 10765 tskmval 10862 cleq1 14962 dfrtrcl2 15041 mrcfval 17587 mrcval 17589 cycsubg2 19164 efgval 19671 lspfval 20856 lspval 20858 lsppropd 20902 aspval 21805 aspval2 21830 clsfval 22928 clsval 22940 clsval2 22953 hauscmplem 23309 cmpfi 23311 1stcfb 23348 fclscmp 23933 scutval 27732 spanval 31142 chsupid 31221 intimafv 32490 fldgenval 32999 primefldgen1 33008 zarclsint 33473 zarcmplem 33482 sigagenval 33759 kur14 34826 mclsval 35173 igenval 37534 pclfvalN 39362 pclvalN 39363 diaintclN 40531 docaffvalN 40594 docafvalN 40595 docavalN 40596 dibintclN 40640 dihglb2 40815 dihintcl 40817 mzpval 42152 dnnumch3lem 42470 aomclem8 42485 rgspnval 42592 rp-intrabeq 42649 nadd1suc 42821 naddsuc2 42822 minregex2 42965 iotain 43854 salgenval 45709 mreclat 48008 |
Copyright terms: Public domain | W3C validator |