![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difeq12d | Structured version Visualization version GIF version |
Description: Equality deduction for class difference. (Contributed by FL, 29-May-2014.) |
Ref | Expression |
---|---|
difeq12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
difeq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
difeq12d | ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difeq12d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | difeq1d 3925 | . 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
3 | difeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | difeq2d 3926 | . 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
5 | 2, 4 | eqtrd 2833 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∖ cdif 3766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rab 3098 df-dif 3772 |
This theorem is referenced by: boxcutc 8191 unfilem3 8468 infdifsn 8804 cantnfp1lem3 8827 infcda1 9303 isf32lem6 9468 isf32lem7 9469 isf32lem8 9470 domtriomlem 9552 domtriom 9553 alephsuc3 9690 symgfixelsi 18167 pmtrprfval 18219 dprdf1o 18747 isirred 19015 isdrng 19069 isdrngd 19090 drngpropd 19092 issubdrg 19123 islbs 19397 lbspropd 19420 lssacsex 19466 lspsnat 19467 frlmlbs 20461 islindf 20476 lindfmm 20491 lsslindf 20494 ptcld 21745 iundisj 23656 iundisj2 23657 iunmbl 23661 volsup 23664 dchrval 25311 nbgrval 26571 nbgr1vtx 26596 iundisjf 29919 iundisj2f 29920 iundisjfi 30073 iundisj2fi 30074 qtophaus 30419 zrhunitpreima 30538 meascnbl 30798 brae 30820 braew 30821 ballotlemfrc 31105 reprdifc 31225 chtvalz 31227 csbdif 33670 poimirlem4 33902 poimirlem6 33904 poimirlem7 33905 poimirlem9 33907 poimirlem13 33911 poimirlem14 33912 poimirlem16 33914 poimirlem19 33917 voliunnfl 33942 itg2addnclem 33949 isdivrngo 34236 drngoi 34237 lsatset 35011 watfvalN 36013 mapdpglem26 37719 mapdpglem27 37720 hvmapffval 37779 hvmapfval 37780 hvmap1o2 37786 dssmapfvd 39093 fzdifsuc2 40269 stoweidlem34 40994 subsalsal 41320 iundjiunlem 41419 iundjiun 41420 meaiuninc 41441 carageniuncllem1 41481 carageniuncl 41483 hspdifhsp 41576 |
Copyright terms: Public domain | W3C validator |