![]() |
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 3175 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4998 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3682 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1536 ∈ wcel 2105 ∀wral 3058 ∩ ciin 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-iin 4998 |
This theorem is referenced by: iinconst 5006 iuniin 5008 iinssiun 5009 iinss1 5011 ssiinf 5058 iinss 5060 iinss2 5061 iinab 5072 iinun2 5077 iundif2 5078 iindif1 5079 iindif2 5081 iinin2 5082 elriin 5085 iinpw 5110 triin 5281 xpiindi 5848 cnviin 6307 iinpreima 7088 iiner 8827 ixpiin 8962 boxriin 8978 iunocv 21716 hauscmplem 23429 txtube 23663 isfcls 24032 iscmet3 25340 taylfval 26414 zarclsiin 33831 fnemeet1 36348 diaglbN 41037 dibglbN 41148 dihglbcpreN 41282 kelac1 43051 eliind 45010 eliuniin 45038 eliin2f 45043 eliinid 45050 eliuniin2 45059 iinssiin 45068 eliind2 45069 iinssf 45077 iindif2f 45102 allbutfi 45342 meaiininclem 46441 hspdifhsp 46571 iinhoiicclem 46628 preimageiingt 46675 preimaleiinlt 46676 smflimlem2 46727 smflimsuplem5 46779 smflimsuplem7 46781 |
Copyright terms: Public domain | W3C validator |