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 4095 | . 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
3 | difeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | difeq2d 4096 | . 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
5 | 2, 4 | eqtrd 2853 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∖ cdif 3930 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 df-dif 3936 |
This theorem is referenced by: boxcutc 8493 unfilem3 8772 infdifsn 9108 cantnfp1lem3 9131 isf32lem6 9768 isf32lem7 9769 isf32lem8 9770 domtriomlem 9852 domtriom 9853 alephsuc3 9990 symgfixelsi 18492 pmtrprfval 18544 dprdf1o 19083 isirred 19378 isdrng 19435 isdrngd 19456 drngpropd 19458 issubdrg 19489 subdrgint 19511 islbs 19777 lbspropd 19800 lssacsex 19845 lspsnat 19846 frlmlbs 20869 islindf 20884 lindfmm 20899 lsslindf 20902 ptcld 22149 iundisj 24076 iundisj2 24077 iunmbl 24081 volsup 24084 dchrval 25737 nbgrval 27045 nbgr1vtx 27067 iundisjf 30267 iundisj2f 30268 iundisjfi 30445 iundisj2fi 30446 lindfpropd 30869 sradrng 30887 qtophaus 30999 zrhunitpreima 31118 meascnbl 31377 brae 31399 braew 31400 ballotlemfrc 31683 reprdifc 31797 chtvalz 31799 satffunlem2lem2 32550 csbdif 34488 poimirlem4 34777 poimirlem6 34779 poimirlem7 34780 poimirlem9 34782 poimirlem13 34786 poimirlem14 34787 poimirlem16 34789 poimirlem19 34792 voliunnfl 34817 itg2addnclem 34824 isdivrngo 35109 drngoi 35110 lsatset 36006 watfvalN 37008 mapdpglem26 38714 mapdpglem27 38715 hvmapffval 38774 hvmapfval 38775 hvmap1o2 38781 prjspval 39131 dssmapfvd 40241 fzdifsuc2 41453 stoweidlem34 42196 subsalsal 42519 iundjiunlem 42618 iundjiun 42619 meaiuninc 42640 carageniuncllem1 42680 carageniuncl 42682 hspdifhsp 42775 |
Copyright terms: Public domain | W3C validator |