![]() |
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 2827 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | notbid 318 | . . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵)) |
3 | 2 | rabbidv 3418 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}) |
4 | dfdif2 3924 | . 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} | |
5 | dfdif2 3924 | . 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵} | |
6 | 3, 4, 5 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ∈ wcel 2107 {crab 3410 ∖ cdif 3912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-dif 3918 |
This theorem is referenced by: difeq12 4082 difeq2i 4084 difeq2d 4087 symdifeq1 4209 ssdifim 4227 disjdif2 4444 ssdifeq0 4449 sorpsscmpl 7676 2oconcl 8454 oev 8465 sbthlem2 9035 sbth 9044 sbthfi 9153 infdiffi 9601 fin1ai 10236 fin23lem7 10259 fin23lem11 10260 compsscnv 10314 isf34lem1 10315 compss 10319 isf34lem4 10320 fin1a2lem7 10349 pwfseqlem4a 10604 pwfseqlem4 10605 efgmval 19501 efgi 19508 frgpuptinv 19560 gsumcllem 19692 gsumzaddlem 19705 selvfval 21543 fctop 22370 cctop 22372 iscld 22394 clsval2 22417 opncldf1 22451 opncldf2 22452 opncldf3 22453 indiscld 22458 mretopd 22459 restcld 22539 lecldbas 22586 pnrmopn 22710 hauscmplem 22773 elpt 22939 elptr 22940 cfinfil 23260 csdfil 23261 ufilss 23272 filufint 23287 cfinufil 23295 ufinffr 23296 ufilen 23297 prdsxmslem2 23901 lebnumlem1 24340 bcth3 24711 ismbl 24906 ishpg 27743 frgrwopregasn 29302 frgrwopregbsn 29303 disjdifprg 31535 0elsiga 32753 prsiga 32770 sigaclci 32771 difelsiga 32772 unelldsys 32797 sigapildsyslem 32800 sigapildsys 32801 ldgenpisyslem1 32802 isros 32807 unelros 32810 difelros 32811 inelsros 32817 diffiunisros 32818 rossros 32819 elcarsg 32945 ballotlemfval 33129 ballotlemgval 33163 kur14lem1 33840 topdifinffinlem 35847 topdifinffin 35848 oe0rif 41649 dssmapfv3d 42365 dssmapnvod 42366 clsk3nimkb 42386 ntrclsneine0lem 42410 ntrclsk2 42414 ntrclskb 42415 ntrclsk13 42417 ntrclsk4 42418 prsal 44633 saldifcl 44634 salexct 44649 salexct2 44654 salexct3 44657 salgencntex 44658 salgensscntex 44659 caragenel 44810 opncldeqv 47008 |
Copyright terms: Public domain | W3C validator |