| 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 4954 | . 2 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} | |
| 2 | nfra1 3286 | . . 3 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 | |
| 3 | 2 | nfab 2928 | . 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| 4 | 1, 3 | nfcxfr 2920 | 1 ⊢ Ⅎ𝑥∩ 𝑥 ∈ 𝐴 𝐵 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ∈ wcel 2145 {cab 2738 Ⅎwnfc 2907 ∀wral 3076 ∩ ciin 4952 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ex 1813 df-nf 1817 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ral 3077 df-iin 4954 |
| This theorem is used by: dmiin 5937 scott0b 9877 scott0OLD 9878 gruiin 10820 zarclsiin 34382 iinssiin 45962 iooiinicc 46373 iooiinioc 46387 fnlimfvre 46503 fnlimabslt 46508 meaiininclem 47315 hspdifhsp 47445 smflimlem2 47601 smflim 47606 smflimmpt 47639 smfsuplem1 47640 smfsupmpt 47644 smfsupxr 47645 smfinflem 47646 smfinfmpt 47648 smflimsuplem7 47655 smflimsuplem8 47656 smflimsupmpt 47658 smfliminfmpt 47661 fsupdm 47671 finfdm 47675 iinfssc 49984 iinfsubc 49985 |
| Copyright terms: Public domain | W3C validator |