![]() |
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 2839 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | 1 | notbid 307 | . . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵)) |
3 | 2 | rabbidv 3339 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}) |
4 | dfdif2 3732 | . 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} | |
5 | dfdif2 3732 | . 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵} | |
6 | 3, 4, 5 | 3eqtr4g 2830 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1631 ∈ wcel 2145 {crab 3065 ∖ cdif 3720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-ral 3066 df-rab 3070 df-dif 3726 |
This theorem is referenced by: difeq12 3874 difeq2i 3876 difeq2d 3879 symdifeq1 3995 ssdifim 4011 disjdif2 4189 ssdifeq0 4193 sorpsscmpl 7095 2oconcl 7737 oev 7748 sbthlem2 8227 sbth 8236 infdiffi 8719 fin1ai 9317 fin23lem7 9340 fin23lem11 9341 compsscnv 9395 isf34lem1 9396 compss 9400 isf34lem4 9401 fin1a2lem7 9430 pwfseqlem4a 9685 pwfseqlem4 9686 efgmval 18332 efgi 18339 frgpuptinv 18391 gsumcllem 18516 gsumzaddlem 18528 fctop 21029 cctop 21031 iscld 21052 clsval2 21075 opncldf1 21109 opncldf2 21110 opncldf3 21111 indiscld 21116 mretopd 21117 restcld 21197 lecldbas 21244 pnrmopn 21368 hauscmplem 21430 elpt 21596 elptr 21597 cfinfil 21917 csdfil 21918 ufilss 21929 filufint 21944 cfinufil 21952 ufinffr 21953 ufilen 21954 prdsxmslem2 22554 lebnumlem1 22980 bcth3 23347 ismbl 23514 ishpg 25872 frgrwopregasn 27498 frgrwopregbsn 27499 disjdifprg 29726 0elsiga 30517 prsiga 30534 sigaclci 30535 difelsiga 30536 unelldsys 30561 sigapildsyslem 30564 sigapildsys 30565 ldgenpisyslem1 30566 isros 30571 unelros 30574 difelros 30575 inelsros 30581 diffiunisros 30582 rossros 30583 elcarsg 30707 ballotlemfval 30891 ballotlemgval 30925 kur14lem1 31526 topdifinffinlem 33532 topdifinffin 33533 dssmapfv3d 38839 dssmapnvod 38840 clsk3nimkb 38864 ntrclsneine0lem 38888 ntrclsk2 38892 ntrclskb 38893 ntrclsk13 38895 ntrclsk4 38896 prsal 41055 saldifcl 41056 salexct 41069 salexct2 41074 salexct3 41077 salgencntex 41078 salgensscntex 41079 caragenel 41229 |
Copyright terms: Public domain | W3C validator |