![]() |
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 3615 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} | |
2 | nfin.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
3 | 2 | nfcri 2787 | . . 3 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
4 | nfin.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
5 | 3, 4 | nfrab 3153 | . 2 ⊢ Ⅎ𝑥{𝑦 ∈ 𝐴 ∣ 𝑦 ∈ 𝐵} |
6 | 1, 5 | nfcxfr 2791 | 1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 Ⅎwnfc 2780 {crab 2945 ∩ cin 3606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-in 3614 |
This theorem is referenced by: csbin 4043 iunxdif3 4638 disjxun 4683 nfres 5430 nfpred 5723 cp 8792 tskwe 8814 iunconn 21279 ptclsg 21466 restmetu 22422 limciun 23703 disjunsn 29533 ordtconnlem1 30098 esum2d 30283 finminlem 32437 mbfposadd 33587 csbingOLD 39369 iunconnlem2 39485 inn0f 39556 disjrnmpt2 39689 disjinfi 39694 fsumiunss 40125 stoweidlem57 40592 fourierdlem80 40721 sge0iunmptlemre 40950 iundjiun 40995 pimiooltgt 41242 smflim 41306 smfpimcclem 41334 smfpimcc 41335 |
Copyright terms: Public domain | W3C validator |