![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfdif | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for class difference. (Contributed by NM, 3-Dec-2003.) (Revised by Mario Carneiro, 13-Oct-2016.) Avoid ax-10 2129, ax-11 2146, ax-12 2166. (Revised by SN, 14-May-2025.) |
Ref | Expression |
---|---|
nfdif.1 | ⊢ Ⅎ𝑥𝐴 |
nfdif.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfdif | ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif 3954 | . . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) | |
2 | nfdif.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2882 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfdif.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2882 | . . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
6 | 5 | nfn 1852 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵 |
7 | 3, 6 | nfan 1894 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) |
8 | 1, 7 | nfxfr 1847 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵) |
9 | 8 | nfci 2878 | 1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 ∈ wcel 2098 Ⅎwnfc 2875 ∖ cdif 3941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-nf 1778 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-v 3463 df-dif 3947 |
This theorem is referenced by: nfsymdif 4245 csbdif 4529 iunxdif3 5099 boxcutc 8960 nfsup 9476 gsum2d2lem 19940 iunconn 23376 iundisj 25521 iundisj2 25522 limciun 25867 difrab2 32374 iundisjf 32458 iundisj2f 32459 suppss2f 32505 aciunf1 32530 iundisjfi 32646 iundisj2fi 32647 fedgmullem2 33459 sigapildsys 33912 vvdifopab 37862 compab 44021 iunconnlem2 44516 supminfxr2 44989 stoweidlem28 45554 stoweidlem34 45560 stoweidlem46 45572 stoweidlem53 45579 stoweidlem55 45581 stoweidlem59 45585 stirlinglem5 45604 preimagelt 46225 preimalegt 46226 |
Copyright terms: Public domain | W3C validator |