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 3166 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}) | |
2 | dfdif2 3549 | . 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} | |
3 | dfdif2 3549 | . 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1475 ∈ wcel 1977 {crab 2900 ∖ 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-nfc 2740 df-rab 2905 df-dif 3543 |
This theorem is referenced by: difeq12 3685 difeq1i 3686 difeq1d 3689 symdifeq1 3808 uneqdifeq 4009 uneqdifeqOLD 4010 hartogslem1 8330 kmlem9 8863 kmlem11 8865 kmlem12 8866 isfin1a 8997 fin1a2lem13 9117 fundmge2nop0 13129 incexclem 14407 coprmprod 15213 coprmproddvds 15215 ismri 16114 f1otrspeq 17690 pmtrval 17694 pmtrfrn 17701 symgsssg 17710 symgfisg 17711 symggen 17713 psgnunilem1 17736 psgnunilem5 17737 psgneldm 17746 ablfac1eulem 18294 islbs 18897 lbsextlem1 18979 lbsextlem2 18980 lbsextlem3 18981 lbsextlem4 18982 zrhcofipsgn 19758 submafval 20204 m1detdiag 20222 lpval 20753 2ndcdisj 21069 isufil 21517 ptcmplem2 21667 mblsplit 23107 voliunlem3 23127 ig1pval 23736 nb3graprlem2 25981 iscusgra 25985 isuvtx 26016 isfrgra 26517 1vwmgra 26530 3vfriswmgra 26532 difeq 28739 sigaval 29500 issiga 29501 issgon 29513 isros 29558 unelros 29561 difelros 29562 inelsros 29568 diffiunisros 29569 rossros 29570 inelcarsg 29700 carsgclctunlem2 29708 probun 29808 ballotlemgval 29912 cvmscbv 30494 cvmsi 30501 cvmsval 30502 poimirlem4 32583 sdrgacs 36790 dssmapfvd 37331 compne 37665 dvmptfprod 38835 caragensplit 39390 vonvolmbllem 39550 vonvolmbl 39551 nbgr2vtx1edg 40572 nbuhgr2vtx1edgb 40574 nbgr0vtx 40578 nb3grprlem2 40609 uvtxa01vtx0 40623 cplgr1v 40652 dfconngr1 41355 isconngr1 41357 isfrgr 41430 frgr1v 41441 nfrgr2v 41442 frgr3v 41445 1vwmgr 41446 3vfriswmgr 41448 ldepsnlinc 42091 |
Copyright terms: Public domain | W3C validator |