Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difeq2 | 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 |
---|---|
difeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2898 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | notbid 319 | . . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵)) |
3 | 2 | rabbidv 3478 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}) |
4 | dfdif2 3942 | . 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} | |
5 | dfdif2 3942 | . 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵} | |
6 | 3, 4, 5 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ∈ wcel 2105 {crab 3139 ∖ 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: difeq12 4091 difeq2i 4093 difeq2d 4096 symdifeq1 4218 ssdifim 4236 disjdif2 4424 ssdifeq0 4428 sorpsscmpl 7449 2oconcl 8117 oev 8128 sbthlem2 8616 sbth 8625 infdiffi 9109 fin1ai 9703 fin23lem7 9726 fin23lem11 9727 compsscnv 9781 isf34lem1 9782 compss 9786 isf34lem4 9787 fin1a2lem7 9816 pwfseqlem4a 10071 pwfseqlem4 10072 efgmval 18767 efgi 18774 frgpuptinv 18826 gsumcllem 18957 gsumzaddlem 18970 selvfval 20258 fctop 21540 cctop 21542 iscld 21563 clsval2 21586 opncldf1 21620 opncldf2 21621 opncldf3 21622 indiscld 21627 mretopd 21628 restcld 21708 lecldbas 21755 pnrmopn 21879 hauscmplem 21942 elpt 22108 elptr 22109 cfinfil 22429 csdfil 22430 ufilss 22441 filufint 22456 cfinufil 22464 ufinffr 22465 ufilen 22466 prdsxmslem2 23066 lebnumlem1 23492 bcth3 23861 ismbl 24054 ishpg 26472 frgrwopregasn 28022 frgrwopregbsn 28023 disjdifprg 30253 0elsiga 31272 prsiga 31289 sigaclci 31290 difelsiga 31291 unelldsys 31316 sigapildsyslem 31319 sigapildsys 31320 ldgenpisyslem1 31321 isros 31326 unelros 31329 difelros 31330 inelsros 31336 diffiunisros 31337 rossros 31338 elcarsg 31462 ballotlemfval 31646 ballotlemgval 31680 kur14lem1 32350 topdifinffinlem 34510 topdifinffin 34511 dssmapfv3d 40243 dssmapnvod 40244 clsk3nimkb 40268 ntrclsneine0lem 40292 ntrclsk2 40296 ntrclskb 40297 ntrclsk13 40299 ntrclsk4 40300 prsal 42480 saldifcl 42481 salexct 42494 salexct2 42499 salexct3 42502 salgencntex 42503 salgensscntex 42504 caragenel 42654 |
Copyright terms: Public domain | W3C validator |