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 3689 | . 2 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)) |
3 | difeq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
4 | 3 | difeq2d 3690 | . 2 ⊢ (𝜑 → (𝐵 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
5 | 2, 4 | eqtrd 2644 | 1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∖ 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-ral 2901 df-rab 2905 df-dif 3543 |
This theorem is referenced by: boxcutc 7837 unfilem3 8111 infdifsn 8437 cantnfp1lem3 8460 infcda1 8898 isf32lem6 9063 isf32lem7 9064 isf32lem8 9065 domtriomlem 9147 domtriom 9148 alephsuc3 9281 symgfixelsi 17678 pmtrprfval 17730 dprdf1o 18254 isirred 18522 isdrng 18574 isdrngd 18595 drngpropd 18597 issubdrg 18628 islbs 18897 lbspropd 18920 lssacsex 18965 lspsnat 18966 frlmlbs 19955 islindf 19970 lindfmm 19985 lsslindf 19988 ptcld 21226 iundisj 23123 iundisj2 23124 iunmbl 23128 volsup 23131 dchrval 24759 iundisjf 28784 iundisj2f 28785 iundisjfi 28942 iundisj2fi 28943 qtophaus 29231 zrhunitpreima 29350 meascnbl 29609 brae 29631 braew 29632 ballotlemfrc 29915 csbdif 32347 poimirlem4 32583 poimirlem6 32585 poimirlem7 32586 poimirlem9 32588 poimirlem13 32592 poimirlem14 32593 poimirlem16 32595 poimirlem19 32598 voliunnfl 32623 itg2addnclem 32631 isdivrngo 32919 drngoi 32920 lsatset 33295 watfvalN 34296 mapdpglem26 36005 mapdpglem27 36006 hvmapffval 36065 hvmapfval 36066 hvmap1o2 36072 dssmapfvd 37331 fzdifsuc2 38466 stoweidlem34 38927 subsalsal 39253 iundjiunlem 39352 iundjiun 39353 meaiuninc 39374 carageniuncllem1 39411 carageniuncl 39413 hspdifhsp 39506 nbgrval 40560 nbgr1vtx 40580 |
Copyright terms: Public domain | W3C validator |