![]() |
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 3442 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}) | |
2 | dfdif2 3954 | . 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} | |
3 | dfdif2 3954 | . 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶} | |
4 | 1, 2, 3 | 3eqtr4g 2793 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ∈ wcel 2099 {crab 3428 ∖ cdif 3942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 df-dif 3948 |
This theorem is referenced by: difeq12 4114 difeq1i 4115 difeq1d 4118 symdifeq1 4241 uneqdifeq 4489 hartogslem1 9560 kmlem9 10176 kmlem11 10178 kmlem12 10179 isfin1a 10310 fin1a2lem13 10430 fundmge2nop0 14480 incexclem 15809 coprmprod 16626 coprmproddvds 16628 ismri 17605 f1otrspeq 19396 pmtrval 19400 pmtrfrn 19407 symgsssg 19416 symgfisg 19417 symggen 19419 psgnunilem1 19442 psgnunilem5 19443 psgneldm 19452 ablfac1eulem 20023 sdrgacs 20683 islbs 20955 lbsextlem1 21040 lbsextlem2 21041 lbsextlem3 21042 lbsextlem4 21043 cofipsgn 21519 selvffval 22053 submafval 22475 m1detdiag 22493 lpval 23037 2ndcdisj 23354 isufil 23801 ptcmplem2 23951 mblsplit 25455 voliunlem3 25475 ig1pval 26104 nbgr2vtx1edg 29157 nbuhgr2vtx1edgb 29159 nbgr0vtx 29163 nb3grprlem2 29188 uvtx01vtx 29204 cplgr1v 29237 dfconngr1 29992 isconngr1 29994 isfrgr 30064 frgr1v 30075 nfrgr2v 30076 frgr3v 30079 1vwmgr 30080 3vfriswmgr 30082 difeq 32309 symgcntz 32803 tocycval 32824 sigaval 33725 issiga 33726 issgon 33737 isros 33782 unelros 33785 difelros 33786 inelsros 33792 diffiunisros 33793 rossros 33794 inelcarsg 33926 carsgclctunlem2 33934 probun 34034 ballotlemgval 34138 cvmscbv 34863 cvmsi 34870 cvmsval 34871 poimirlem4 37092 dssmapfvd 43438 compne 43869 dvmptfprod 45324 caragensplit 45879 vonvolmbllem 46039 vonvolmbl 46040 ldepsnlinc 47567 eenglngeehlnm 47803 |
Copyright terms: Public domain | W3C validator |