![]() |
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 4120 | . 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
3 | difeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | difeq2d 4121 | . 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
5 | 2, 4 | eqtrd 2766 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∖ cdif 3944 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-dif 3950 |
This theorem is referenced by: csbdif 4532 xpord2pred 8159 xpord3pred 8166 boxcutc 8970 unfilem3 9346 infdifsn 9700 cantnfp1lem3 9723 isf32lem6 10401 isf32lem7 10402 isf32lem8 10403 domtriomlem 10485 domtriom 10486 alephsuc3 10623 symgfixelsi 19433 pmtrprfval 19485 dprdf1o 20032 isirred 20401 isdrng 20711 isdrngd 20743 isdrngdOLD 20745 drngpropd 20747 issubdrg 20759 subdrgint 20782 islbs 21054 lbspropd 21077 lssacsex 21125 lspsnat 21126 frlmlbs 21795 islindf 21810 lindfmm 21825 lsslindf 21828 psdmullem 22159 ptcld 23608 iundisj 25568 iundisj2 25569 iunmbl 25573 volsup 25576 dchrval 27263 newval 27879 sltlpss 27930 slelss 27931 nbgrval 29272 nbgr1vtx 29294 iundisjf 32509 iundisj2f 32510 iundisjfi 32698 iundisj2fi 32699 lindfpropd 33257 opprqusdrng 33368 rprmval 33391 isufd 33415 sradrng 33480 qtophaus 33651 zrhunitpreima 33793 meascnbl 34052 brae 34074 braew 34075 ballotlemfrc 34360 reprdifc 34473 chtvalz 34475 satffunlem2lem2 35234 poimirlem4 37325 poimirlem6 37327 poimirlem7 37328 poimirlem9 37330 poimirlem13 37334 poimirlem14 37335 poimirlem16 37337 poimirlem19 37340 voliunnfl 37365 itg2addnclem 37372 isdivrngo 37651 drngoi 37652 lsatset 38688 watfvalN 39691 mapdpglem26 41397 mapdpglem27 41398 hvmapffval 41457 hvmapfval 41458 hvmap1o2 41464 prjspval 42257 prjspnvs 42274 cantnfresb 42990 tfsconcatun 43003 tfsconcat0i 43011 dssmapfvd 43684 fzdifsuc2 44925 stoweidlem34 45655 subsalsal 45980 iundjiunlem 46080 iundjiun 46081 meaiuninc 46102 carageniuncllem1 46142 carageniuncl 46144 hspdifhsp 46237 |
Copyright terms: Public domain | W3C validator |