![]() |
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 2877 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) | |
2 | 1 | ralbidv 3162 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
3 | df-iin 4884 | . 2 ⊢ ∩ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝐶} | |
4 | 2, 3 | elab2g 3616 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∩ ciin 4882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-iin 4884 |
This theorem is referenced by: iinconst 4891 iuniin 4893 iinssiun 4894 iinss1 4896 ssiinf 4941 iinss 4943 iinss2 4944 iinab 4953 iinun2 4958 iundif2 4959 iindif1 4960 iindif2 4962 iinin2 4963 elriin 4966 iinpw 4991 triin 5151 xpiindi 5670 cnviin 6105 iinpreima 6814 iiner 8352 ixpiin 8471 boxriin 8487 iunocv 20370 hauscmplem 22011 txtube 22245 isfcls 22614 iscmet3 23897 taylfval 24954 zarclsiin 31224 fnemeet1 33827 diaglbN 38351 dibglbN 38462 dihglbcpreN 38596 kelac1 40007 eliind 41705 eliuniin 41735 eliin2f 41740 eliinid 41747 eliuniin2 41755 iinssiin 41764 eliind2 41765 iinssf 41775 allbutfi 42029 meaiininclem 43125 hspdifhsp 43255 iinhoiicclem 43312 preimageiingt 43355 preimaleiinlt 43356 smflimlem2 43405 smflimsuplem5 43455 smflimsuplem7 43457 |
Copyright terms: Public domain | W3C validator |