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 4924 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | nfra1 3221 | . . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
3 | 2 | nfab 2986 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
4 | 1, 3 | nfcxfr 2977 | 1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 {cab 2801 Ⅎwnfc 2963 ∀wral 3140 ∩ ciin 4922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-iin 4924 |
This theorem is referenced by: dmiin 5827 scott0 9317 gruiin 10234 iinssiin 41402 iooiinicc 41825 iooiinioc 41839 fnlimfvre 41962 fnlimabslt 41967 meaiininclem 42775 hspdifhsp 42905 smflimlem2 43055 smflim 43060 smflimmpt 43091 smfsuplem1 43092 smfsupmpt 43096 smfsupxr 43097 smfinflem 43098 smfinfmpt 43100 smflimsuplem7 43107 smflimsuplem8 43108 smflimsupmpt 43110 smfliminfmpt 43113 |
Copyright terms: Public domain | W3C validator |