Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ineq1i | Structured version Visualization version GIF version |
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.) |
Ref | Expression |
---|---|
ineq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
ineq1i | ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | ineq1 4178 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∩ cin 3932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 df-in 3940 |
This theorem is referenced by: in12 4194 inindi 4200 dfrab3 4275 dfif5 4479 disjpr2 4641 disjtpsn 4643 disjtp2 4644 resres 5859 imainrect 6031 predidm 6163 fresaun 6542 fresaunres2 6543 ssenen 8679 hartogslem1 8994 prinfzo0 13064 leiso 13805 f1oun2prg 14267 smumul 15830 setsfun 16506 setsfun0 16507 firest 16694 lsmdisj2r 18740 frgpuplem 18827 ltbwe 20181 tgrest 21695 fiuncmp 21940 ptclsg 22151 metnrmlem3 23396 mbfid 24163 ppi1 25668 cht1 25669 ppiub 25707 chdmj2i 29186 chjassi 29190 pjoml2i 29289 pjoml4i 29291 cmcmlem 29295 mayetes3i 29433 cvmdi 30028 atomli 30086 atabsi 30105 uniin1 30230 disjuniel 30275 imadifxp 30279 gtiso 30362 prsss 31058 ordtrest2NEW 31065 esumnul 31206 measinblem 31378 eulerpartlemt 31528 ballotlem2 31645 ballotlemfp1 31648 ballotlemfval0 31652 chtvalz 31799 fmla0disjsuc 32542 mthmpps 32726 dffv5 33282 bj-sscon 34238 bj-discrmoore 34297 mblfinlem2 34811 ismblfin 34814 mbfposadd 34820 itg2addnclem2 34825 asindmre 34858 abeqin 35395 xrnres 35530 redundeq1 35744 refrelsredund4 35747 diophrw 39234 dnwech 39526 lmhmlnmsplit 39565 rp-fakeuninass 39760 iunrelexp0 39925 nznngen 40525 uzinico2 41714 limsup0 41851 limsupvaluz 41865 sge0sn 42538 31prm 43637 |
Copyright terms: Public domain | W3C validator |