![]() |
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 4555 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
2 | nfra1 2970 | . . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
3 | 2 | nfab 2798 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
4 | 1, 3 | nfcxfr 2791 | 1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 {cab 2637 Ⅎwnfc 2780 ∀wral 2941 ∩ ciin 4553 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-iin 4555 |
This theorem is referenced by: dmiin 5401 scott0 8787 gruiin 9670 iinssiin 39626 iooiinicc 40087 iooiinioc 40101 fnlimfvre 40224 fnlimabslt 40229 meaiininclem 41021 hspdifhsp 41151 smflimlem2 41301 smflim 41306 smflimmpt 41337 smfsuplem1 41338 smfsupmpt 41342 smfsupxr 41343 smfinflem 41344 smfinfmpt 41346 smflimsuplem7 41353 smflimsuplem8 41354 smflimsupmpt 41356 smfliminfmpt 41359 |
Copyright terms: Public domain | W3C validator |