| 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 2178, ax-11 2194, ax-12 2215. (Revised by SN, 14-May-2025.) |
| Ref | Expression |
|---|---|
| nfdif.1 | ⊢ Ⅎ𝑥𝐴 |
| nfdif.2 | ⊢ Ⅎ𝑥𝐵 |
| Ref | Expression |
|---|---|
| nfdif | ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldif 3917 | . . 3 ⊢ (𝑦 ∈ (𝐴 ∖ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵)) | |
| 2 | nfdif.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | nfcri 2919 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
| 4 | nfdif.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
| 5 | 4 | nfcri 2919 | . . . . 5 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
| 6 | 5 | nfn 1880 | . . . 4 ⊢ Ⅎ𝑥 ¬ 𝑦 ∈ 𝐵 |
| 7 | 3, 6 | nfan 1922 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵) |
| 8 | 1, 7 | nfxfr 1876 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∖ 𝐵) |
| 9 | 8 | nfci 2915 | 1 ⊢ Ⅎ𝑥(𝐴 ∖ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∧ wa 400 ∈ wcel 2145 Ⅎwnfc 2912 ∖ cdif 3904 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-tru 1566 df-ex 1803 df-nf 1807 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-v 3459 df-dif 3910 |
| This theorem is referenced by: nfsymdif 4212 csbdif 4482 iunxdif3 5057 boxcutc 8927 nfsup 9399 gsum2d2lem 20034 iunconn 23546 iundisj 25668 iundisj2 25669 limciun 26014 difrab2 32754 iundisjf 32844 iundisj2f 32845 suppss2f 32895 aciunf1 32920 iundisjfi 33053 iundisj2fi 33054 suppgsumssiun 33305 fedgmullem2 33937 sigapildsys 34469 vvdifopab 38776 compab 45015 iunconnlem2 45508 supminfxr2 46041 stoweidlem28 46600 stoweidlem34 46606 stoweidlem46 46618 stoweidlem53 46625 stoweidlem55 46627 stoweidlem59 46631 stirlinglem5 46650 preimagelt 47271 preimalegt 47272 |
| Copyright terms: Public domain | W3C validator |