![]() |
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.) Avoid ax-10 2130, ax-11 2147, ax-12 2167. (Revised by SN, 14-May-2025.) |
Ref | Expression |
---|---|
nfin.1 | ⊢ Ⅎ𝑥𝐴 |
nfin.2 | ⊢ Ⅎ𝑥𝐵 |
Ref | Expression |
---|---|
nfin | ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3963 | . . 3 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
2 | nfin.1 | . . . . 5 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2883 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
4 | nfin.2 | . . . . 5 ⊢ Ⅎ𝑥𝐵 | |
5 | 4 | nfcri 2883 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 |
6 | 3, 5 | nfan 1895 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
7 | 1, 6 | nfxfr 1848 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∩ 𝐵) |
8 | 7 | nfci 2879 | 1 ⊢ Ⅎ𝑥(𝐴 ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∈ wcel 2099 Ⅎwnfc 2876 ∩ cin 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-v 3464 df-in 3954 |
This theorem is referenced by: inn0f 4371 csbin 4444 iunxdif3 5103 disjxun 5151 nfres 5991 nfpred 6317 cp 9934 tskwe 9993 iunconn 23423 ptclsg 23610 restmetu 24570 limciun 25914 disjunsn 32514 ordtconnlem1 33739 esum2d 33926 finminlem 36030 bj-rcleqf 36732 mbfposadd 37368 iunconnlem2 44611 disjrnmpt2 44795 disjinfi 44799 fsumiunss 45196 stoweidlem57 45678 fourierdlem80 45807 sge0iunmptlemre 46036 iundjiun 46081 pimiooltgt 46331 smflim 46398 smfpimcclem 46428 smfpimcc 46429 adddmmbl 46454 adddmmbl2 46455 muldmmbl 46456 muldmmbl2 46457 smfdivdmmbl2 46462 |
Copyright terms: Public domain | W3C validator |