![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
difeq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeq 3401 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}) | |
2 | dfdif2 3833 | . 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} | |
3 | dfdif2 3833 | . 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2834 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1508 ∈ wcel 2051 {crab 3087 ∖ cdif 3821 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-rab 3092 df-dif 3827 |
This theorem is referenced by: difeq12 3979 difeq1i 3980 difeq1d 3983 symdifeq1 4103 uneqdifeq 4316 hartogslem1 8800 kmlem9 9377 kmlem11 9379 kmlem12 9380 isfin1a 9511 fin1a2lem13 9631 fundmge2nop0 13660 incexclem 15050 coprmprod 15860 coprmproddvds 15862 ismri 16773 f1otrspeq 18349 pmtrval 18353 pmtrfrn 18360 symgsssg 18369 symgfisg 18370 symggen 18372 psgnunilem1 18395 psgnunilem5 18396 psgnunilem5OLD 18397 psgneldm 18406 ablfac1eulem 18957 sdrgacs 19315 islbs 19583 lbsextlem1 19665 lbsextlem2 19666 lbsextlem3 19667 lbsextlem4 19668 cofipsgn 20455 submafval 20908 m1detdiag 20926 lpval 21467 2ndcdisj 21784 isufil 22231 ptcmplem2 22381 mblsplit 23852 voliunlem3 23872 ig1pval 24485 nbgr2vtx1edg 26851 nbuhgr2vtx1edgb 26853 nbgr0vtx 26857 nb3grprlem2 26882 uvtx01vtx 26898 cplgr1v 26931 dfconngr1 27733 isconngr1 27735 isfrgr 27808 frgr1v 27821 nfrgr2v 27822 frgr3v 27825 1vwmgr 27826 3vfriswmgr 27828 difeq 30072 tocycval 30473 sigaval 31047 issiga 31048 issgon 31060 isros 31105 unelros 31108 difelros 31109 inelsros 31115 diffiunisros 31116 rossros 31117 inelcarsg 31247 carsgclctunlem2 31255 probun 31356 ballotlemgval 31460 cvmscbv 32123 cvmsi 32130 cvmsval 32131 poimirlem4 34370 dssmapfvd 39760 compne 40225 compneOLD 40226 dvmptfprod 41690 caragensplit 42243 vonvolmbllem 42403 vonvolmbl 42404 ldepsnlinc 43960 eenglngeehlnm 44124 |
Copyright terms: Public domain | W3C validator |