Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfin | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) |
Ref | Expression |
---|---|
nfin.1 | ⊢ Ⅎ𝑥𝐴 |
nfin.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfin | ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfin5 3548 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} | |
2 | nfin.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2745 | . . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | nfin.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
5 | 3, 4 | nfrab 3100 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} |
6 | 1, 5 | nfcxfr 2749 | 1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Ⅎwnfc 2738 {crab 2900 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-in 3547 |
This theorem is referenced by: csbin 3962 iunxdif3 4542 disjxun 4581 nfres 5319 nfpred 5602 cp 8637 tskwe 8659 iuncon 21041 ptclsg 21228 restmetu 22185 limciun 23464 disjunsn 28789 ordtconlem1 29298 esum2d 29482 finminlem 31482 mbfposadd 32627 csbingOLD 38076 iunconlem2 38193 inn0f 38268 disjrnmpt2 38370 disjinfi 38375 fsumiunss 38642 stoweidlem57 38950 fourierdlem80 39079 sge0iunmptlemre 39308 iundjiun 39353 pimiooltgt 39598 smflim 39663 |
Copyright terms: Public domain | W3C validator |