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 2676 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 2969 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4458 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3322 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∩ ciin 4456 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 df-iin 4458 |
This theorem is referenced by: iinconst 4466 iuniin 4467 iinss1 4469 ssiinf 4505 iinss 4507 iinss2 4508 iinab 4517 iinun2 4522 iundif2 4523 iindif2 4525 iinin2 4526 elriin 4529 iinpw 4550 xpiindi 5179 cnviin 5589 iinpreima 6253 iiner 7706 ixpiin 7820 boxriin 7836 iunocv 19844 hauscmplem 21019 txtube 21253 isfcls 21623 iscmet3 22899 taylfval 23917 fnemeet1 31531 diaglbN 35362 dibglbN 35473 dihglbcpreN 35607 kelac1 36651 eliind 38266 eliuniin 38307 eliin2f 38316 eliinid 38325 eliuniin2 38335 allbutfi 38557 meaiininclem 39376 hspdifhsp 39506 iinhoiicclem 39564 preimageiingt 39607 preimaleiinlt 39608 smflimlem2 39658 |
Copyright terms: Public domain | W3C validator |