| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eliin | Structured version Visualization version GIF version | ||
| Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.) |
| Ref | Expression |
|---|---|
| eliin | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 2829 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
| 2 | 1 | ralbidv 3178 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
| 3 | df-iin 4994 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
| 4 | 2, 3 | elab2g 3680 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∩ ciin 4992 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-iin 4994 |
| This theorem is referenced by: iinconst 5002 iuniin 5004 iinssiun 5005 iinss1 5007 ssiinf 5054 iinss 5056 iinss2 5057 iinab 5068 iinun2 5073 iundif2 5074 iindif1 5075 iindif2 5077 iinin2 5078 elriin 5081 iinpw 5106 triin 5276 xpiindi 5846 cnviin 6306 iinpreima 7089 iiner 8829 ixpiin 8964 boxriin 8980 iunocv 21699 hauscmplem 23414 txtube 23648 isfcls 24017 iscmet3 25327 taylfval 26400 zarclsiin 33870 fnemeet1 36367 diaglbN 41057 dibglbN 41168 dihglbcpreN 41302 kelac1 43075 eliind 45076 eliuniin 45104 eliin2f 45109 eliinid 45116 eliuniin2 45125 iinssiin 45134 eliind2 45135 iinssf 45143 iindif2f 45165 allbutfi 45404 meaiininclem 46501 hspdifhsp 46631 iinhoiicclem 46688 preimageiingt 46735 preimaleiinlt 46736 smflimlem2 46787 smflimsuplem5 46839 smflimsuplem7 46841 |
| Copyright terms: Public domain | W3C validator |