![]() |
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 3800 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} | |
2 | nfin.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2929 | . . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | nfin.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
5 | 3, 4 | nfrab 3310 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} |
6 | 1, 5 | nfcxfr 2932 | 1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Ⅎwnfc 2919 {crab 3094 ∩ cin 3791 |
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-in 3799 |
This theorem is referenced by: csbin 4236 iunxdif3 4840 disjxun 4884 nfres 5644 nfpred 5938 cp 9051 tskwe 9109 iunconn 21640 ptclsg 21827 restmetu 22783 limciun 24095 disjunsn 29970 ordtconnlem1 30568 esum2d 30753 finminlem 32901 mbfposadd 34084 iunconnlem2 40108 inn0f 40177 disjrnmpt2 40302 disjinfi 40307 fsumiunss 40719 stoweidlem57 41205 fourierdlem80 41334 sge0iunmptlemre 41560 iundjiun 41605 pimiooltgt 41852 smflim 41916 smfpimcclem 41944 smfpimcc 41945 |
Copyright terms: Public domain | W3C validator |