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 3583 | . 2 ⊢ (𝐴 ∖ 𝐵) = {𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} | |
2 | nfdif.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2758 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | 3 | nfn 1784 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵 |
5 | nfdif.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
6 | 4, 5 | nfrab 3123 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2762 | 1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 1990 Ⅎwnfc 2751 {crab 2916 ∖ cdif 3571 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-dif 3577 |
This theorem is referenced by: nfsymdif 3848 iunxdif3 4606 boxcutc 7951 nfsup 8357 gsum2d2lem 18372 iunconn 21231 iundisj 23316 iundisj2 23317 limciun 23658 difrab2 29339 iundisjf 29402 iundisj2f 29403 suppss2f 29439 aciunf1 29463 iundisjfi 29555 iundisj2fi 29556 sigapildsys 30225 csbdif 33171 vvdifopab 34024 compab 38645 iunconnlem2 39171 supminfxr2 39699 stoweidlem28 40245 stoweidlem34 40251 stoweidlem46 40263 stoweidlem53 40270 stoweidlem55 40272 stoweidlem59 40276 stirlinglem5 40295 preimagelt 40912 preimalegt 40913 |
Copyright terms: Public domain | W3C validator |