![]() |
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 5024 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
Ref | Expression |
---|---|
nfiun.1 | ⊢ Ⅎ𝑦𝐴 |
nfiun.2 | ⊢ Ⅎ𝑦𝐵 |
Ref | Expression |
---|---|
nfiin | ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iin 4994 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
2 | nfiun.1 | . . . 4 ⊢ Ⅎ𝑦𝐴 | |
3 | nfiun.2 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
4 | 3 | nfcri 2885 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
5 | 2, 4 | nfralw 3303 | . . 3 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 |
6 | 5 | nfab 2904 | . 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} |
7 | 1, 6 | nfcxfr 2896 | 1 ⊢ Ⅎ𝑦∩ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 {cab 2704 Ⅎwnfc 2878 ∀wral 3056 ∩ ciin 4992 |
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 2164 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ral 3057 df-iin 4994 |
This theorem is referenced by: iinab 5065 fnlimcnv 44978 fnlimfvre 44985 fnlimabslt 44990 iinhoiicc 45985 preimageiingt 46031 preimaleiinlt 46032 smflimlem6 46087 smflim 46088 smflim2 46117 smfsup 46125 smfsupmpt 46126 smfsupxr 46127 smfinflem 46128 smfinf 46129 smfinfmpt 46130 smflimsup 46139 smfliminf 46142 fsupdm 46153 finfdm 46157 |
Copyright terms: Public domain | W3C validator |