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 2826 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 3119 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4921 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3601 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∈ wcel 2111 ∀wral 3062 ∩ ciin 4919 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-iin 4921 |
This theorem is referenced by: iinconst 4928 iuniin 4930 iinssiun 4931 iinss1 4933 ssiinf 4977 iinss 4979 iinss2 4980 iinab 4990 iinun2 4995 iundif2 4996 iindif1 4997 iindif2 4999 iinin2 5000 elriin 5003 iinpw 5028 triin 5190 xpiindi 5718 cnviin 6163 iinpreima 6907 iiner 8491 ixpiin 8625 boxriin 8641 iunocv 20667 hauscmplem 22327 txtube 22561 isfcls 22930 iscmet3 24214 taylfval 25275 zarclsiin 31559 fnemeet1 34318 diaglbN 38832 dibglbN 38943 dihglbcpreN 39077 kelac1 40619 eliind 42320 eliuniin 42350 eliin2f 42355 eliinid 42362 eliuniin2 42370 iinssiin 42379 eliind2 42380 iinssf 42388 allbutfi 42634 meaiininclem 43727 hspdifhsp 43857 iinhoiicclem 43914 preimageiingt 43957 preimaleiinlt 43958 smflimlem2 44007 smflimsuplem5 44057 smflimsuplem7 44059 |
Copyright terms: Public domain | W3C validator |