![]() |
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 2847 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 3168 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4758 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3561 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ∈ wcel 2107 ∀wral 3090 ∩ ciin 4756 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-v 3400 df-iin 4758 |
This theorem is referenced by: iinconst 4765 iuniin 4766 iinss1 4768 ssiinf 4804 iinss 4806 iinss2 4807 iinab 4816 iinun2 4821 iundif2 4822 iindif2 4824 iinin2 4825 elriin 4828 iinpw 4853 triin 5004 xpiindi 5505 cnviin 5928 iinpreima 6611 iiner 8104 ixpiin 8222 boxriin 8238 iunocv 20435 hauscmplem 21629 txtube 21863 isfcls 22232 iscmet3 23510 taylfval 24561 iinssiun 29956 fnemeet1 32957 diaglbN 37218 dibglbN 37329 dihglbcpreN 37463 kelac1 38606 eliind 40185 eliuniin 40224 eliin2f 40230 eliinid 40237 eliuniin2 40246 iinssiin 40254 eliind2 40255 iinssf 40267 allbutfi 40536 meaiininclem 41641 hspdifhsp 41771 iinhoiicclem 41828 preimageiingt 41871 preimaleiinlt 41872 smflimlem2 41921 smflimsuplem5 41971 smflimsuplem7 41973 |
Copyright terms: Public domain | W3C validator |