| 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 3451 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}) | |
| 2 | dfdif2 3960 | . 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} | |
| 3 | dfdif2 3960 | . 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶} | |
| 4 | 1, 2, 3 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ∈ wcel 2108 {crab 3436 ∖ cdif 3948 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-dif 3954 |
| This theorem is referenced by: difeq12 4121 difeq1i 4122 difeq1d 4125 symdifeq1 4255 uneqdifeq 4493 hartogslem1 9582 kmlem9 10199 kmlem11 10201 kmlem12 10202 isfin1a 10332 fin1a2lem13 10452 fundmge2nop0 14541 incexclem 15872 coprmprod 16698 coprmproddvds 16700 ismri 17674 f1otrspeq 19465 pmtrval 19469 pmtrfrn 19476 symgsssg 19485 symgfisg 19486 symggen 19488 psgnunilem1 19511 psgnunilem5 19512 psgneldm 19521 ablfac1eulem 20092 sdrgacs 20802 islbs 21075 lbsextlem1 21160 lbsextlem2 21161 lbsextlem3 21162 lbsextlem4 21163 cofipsgn 21611 selvffval 22137 submafval 22585 m1detdiag 22603 lpval 23147 2ndcdisj 23464 isufil 23911 ptcmplem2 24061 mblsplit 25567 voliunlem3 25587 ig1pval 26215 nbgr2vtx1edg 29367 nbuhgr2vtx1edgb 29369 nb3grprlem2 29398 uvtx01vtx 29414 cplgr1v 29447 dfconngr1 30207 isconngr1 30209 isfrgr 30279 frgr1v 30290 nfrgr2v 30291 frgr3v 30294 1vwmgr 30295 3vfriswmgr 30297 difeq 32537 symgcntz 33105 tocycval 33128 sigaval 34112 issiga 34113 issgon 34124 isros 34169 unelros 34172 difelros 34173 inelsros 34179 diffiunisros 34180 rossros 34181 inelcarsg 34313 carsgclctunlem2 34321 probun 34421 ballotlemgval 34526 cvmscbv 35263 cvmsi 35270 cvmsval 35271 poimirlem4 37631 dssmapfvd 44030 compne 44460 dvmptfprod 45960 caragensplit 46515 vonvolmbllem 46675 vonvolmbl 46676 ldepsnlinc 48425 eenglngeehlnm 48660 |
| Copyright terms: Public domain | W3C validator |