![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfii1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by NM, 15-Oct-2003.) |
Ref | Expression |
---|---|
nfii1 | ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iin 4957 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | nfra1 3267 | . . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
3 | 2 | nfab 2913 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
4 | 1, 3 | nfcxfr 2905 | 1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 {cab 2713 Ⅎwnfc 2887 ∀wral 3064 ∩ ciin 4955 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ral 3065 df-iin 4957 |
This theorem is referenced by: dmiin 5908 scott0 9822 gruiin 10746 zarclsiin 32452 iinssiin 43329 iooiinicc 43770 iooiinioc 43784 fnlimfvre 43905 fnlimabslt 43910 meaiininclem 44717 hspdifhsp 44847 smflimlem2 45003 smflim 45008 smflimmpt 45041 smfsuplem1 45042 smfsupmpt 45046 smfsupxr 45047 smfinflem 45048 smfinfmpt 45050 smflimsuplem7 45057 smflimsuplem8 45058 smflimsupmpt 45060 smfliminfmpt 45063 fsupdm 45073 finfdm 45077 |
Copyright terms: Public domain | W3C validator |