![]() |
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.) |
Ref | Expression |
---|---|
nfdif.1 | ⊢ Ⅎ𝑥𝐴 |
nfdif.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfdif | ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdif2 3801 | . 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} | |
2 | nfdif.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2929 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | 3 | nfn 1902 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵 |
5 | nfdif.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
6 | 4, 5 | nfrab 3310 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2932 | 1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2107 Ⅎwnfc 2919 {crab 3094 ∖ cdif 3789 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-dif 3795 |
This theorem is referenced by: nfsymdif 4071 iunxdif3 4842 boxcutc 8239 nfsup 8647 gsum2d2lem 18769 iunconn 21651 iundisj 23763 iundisj2 23764 limciun 24106 difrab2 29918 iundisjf 29982 iundisj2f 29983 suppss2f 30021 aciunf1 30045 iundisjfi 30133 iundisj2fi 30134 sigapildsys 30831 csbdif 33774 vvdifopab 34668 compab 39614 iunconnlem2 40118 supminfxr2 40618 stoweidlem28 41186 stoweidlem34 41192 stoweidlem46 41204 stoweidlem53 41211 stoweidlem55 41213 stoweidlem59 41217 stirlinglem5 41236 preimagelt 41853 preimalegt 41854 |
Copyright terms: Public domain | W3C validator |