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 3880 | . 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} | |
2 | nfdif.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2891 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | 3 | nfn 1865 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵 |
5 | nfdif.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
6 | 4, 5 | nfrabw 3302 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2902 | 1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2110 Ⅎwnfc 2884 {crab 3065 ∖ cdif 3868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-rab 3070 df-dif 3874 |
This theorem is referenced by: nfsymdif 4166 iunxdif3 5008 boxcutc 8627 nfsup 9072 gsum2d2lem 19363 iunconn 22330 iundisj 24450 iundisj2 24451 limciun 24796 difrab2 30569 iundisjf 30652 iundisj2f 30653 suppss2f 30698 aciunf1 30725 iundisjfi 30842 iundisj2fi 30843 fedgmullem2 31430 sigapildsys 31847 csbdif 35238 vvdifopab 36141 compab 41741 iunconnlem2 42236 supminfxr2 42692 stoweidlem28 43252 stoweidlem34 43258 stoweidlem46 43270 stoweidlem53 43277 stoweidlem55 43279 stoweidlem59 43283 stirlinglem5 43302 preimagelt 43919 preimalegt 43920 |
Copyright terms: Public domain | W3C validator |