![]() |
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 2867 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 3168 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4714 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3546 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 ∈ wcel 2157 ∀wral 3090 ∩ ciin 4712 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 df-v 3388 df-iin 4714 |
This theorem is referenced by: iinconst 4721 iuniin 4722 iinss1 4724 ssiinf 4760 iinss 4762 iinss2 4763 iinab 4772 iinun2 4777 iundif2 4778 iindif2 4780 iinin2 4781 elriin 4784 iinpw 4809 triin 4961 xpiindi 5462 cnviin 5892 iinpreima 6572 iiner 8058 ixpiin 8175 boxriin 8191 iunocv 20349 hauscmplem 21537 txtube 21771 isfcls 22140 iscmet3 23418 taylfval 24453 iinssiun 29893 fnemeet1 32872 diaglbN 37075 dibglbN 37186 dihglbcpreN 37320 kelac1 38413 eliind 39994 eliuniin 40033 eliin2f 40040 eliinid 40047 eliuniin2 40056 iinssiin 40064 eliind2 40065 iinssf 40079 allbutfi 40354 meaiininclem 41441 hspdifhsp 41571 iinhoiicclem 41628 preimageiingt 41671 preimaleiinlt 41672 smflimlem2 41721 smflimsuplem5 41771 smflimsuplem7 41773 |
Copyright terms: Public domain | W3C validator |