![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfiin | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2366. See nfiing 5027 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfiun.1 | ⊢ Ⅎ𝑦𝐴 |
nfiun.2 | ⊢ Ⅎ𝑦𝐵 |
Ref | Expression |
---|---|
nfiin | ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iin 4997 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
2 | nfiun.1 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | nfiun.2 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
4 | 3 | nfcri 2883 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
5 | 2, 4 | nfralw 3299 | . . 3 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 |
6 | 5 | nfab 2898 | . 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2890 | 1 ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 {cab 2703 Ⅎwnfc 2876 ∀wral 3051 ∩ ciin 4995 |
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-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-iin 4997 |
This theorem is referenced by: iinab 5069 fnlimcnv 45322 fnlimfvre 45329 fnlimabslt 45334 iinhoiicc 46329 preimageiingt 46375 preimaleiinlt 46376 smflimlem6 46431 smflim 46432 smflim2 46461 smfsup 46469 smfsupmpt 46470 smfsupxr 46471 smfinflem 46472 smfinf 46473 smfinfmpt 46474 smflimsup 46483 smfliminf 46486 fsupdm 46497 finfdm 46501 |
Copyright terms: Public domain | W3C validator |