Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difeq2i | Structured version Visualization version GIF version |
Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.) |
Ref | Expression |
---|---|
difeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
difeq2i | ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | difeq2 3684 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∖ cdif 3537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-ral 2901 df-rab 2905 df-dif 3543 |
This theorem is referenced by: difeq12i 3688 dfun3 3824 dfin3 3825 dfin4 3826 invdif 3827 indif 3828 difundi 3838 difindi 3840 difdif2 3843 dif32 3850 difabs 3851 dfsymdif3 3852 notrab 3863 dif0 3904 unvdif 3994 difdifdir 4008 dfif3 4050 difpr 4275 iinvdif 4528 cnvin 5459 fndifnfp 6347 dif1o 7467 dfsdom2 7968 cda1dif 8881 m1bits 15000 clsval2 20664 mretopd 20706 cmpfi 21021 llycmpkgen2 21163 pserdvlem2 23986 nbgrassvwo2 25967 clwlknclwlkdifs 26487 frgraregorufr0 26579 iundifdifd 28762 iundifdif 28763 difres 28795 sibfof 29729 eulerpartlemmf 29764 kur14lem2 30443 kur14lem6 30447 kur14lem7 30448 dfon4 31170 onint1 31618 bj-2upln1upl 32205 poimirlem8 32587 diophren 36395 nonrel 36909 dssmapntrcls 37446 salincl 39219 meaiuninc 39374 carageniuncllem1 39411 nbgrssvwo2 40587 clwwlknclwwlkdifs 41181 frgrregorufr0 41489 |
Copyright terms: Public domain | W3C validator |