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 2897 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 3194 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4913 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3665 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 ∀wral 3135 ∩ ciin 4911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-iin 4913 |
This theorem is referenced by: iinconst 4920 iuniin 4922 iinssiun 4923 iinss1 4925 ssiinf 4969 iinss 4971 iinss2 4972 iinab 4981 iinun2 4986 iundif2 4987 iindif1 4988 iindif2 4990 iinin2 4991 elriin 4994 iinpw 5019 triin 5178 xpiindi 5699 cnviin 6130 iinpreima 6829 iiner 8358 ixpiin 8476 boxriin 8492 iunocv 20753 hauscmplem 21942 txtube 22176 isfcls 22545 iscmet3 23823 taylfval 24874 fnemeet1 33611 diaglbN 38071 dibglbN 38182 dihglbcpreN 38316 kelac1 39541 eliind 41210 eliuniin 41242 eliin2f 41247 eliinid 41254 eliuniin2 41263 iinssiin 41271 eliind2 41272 iinssf 41283 allbutfi 41541 meaiininclem 42645 hspdifhsp 42775 iinhoiicclem 42832 preimageiingt 42875 preimaleiinlt 42876 smflimlem2 42925 smflimsuplem5 42975 smflimsuplem7 42977 |
Copyright terms: Public domain | W3C validator |