![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elintg | Structured version Visualization version GIF version |
Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.) |
Ref | Expression |
---|---|
elintg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2822 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
2 | 1 | ralbidv 3178 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
3 | dfint2 4953 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
4 | 2, 3 | elab2g 3671 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∩ cint 4951 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-int 4952 |
This theorem is referenced by: elinti 4960 elintabg 4962 elrint 4996 onmindif 6457 onmindif2 7795 mremre 17548 toponmre 22597 1stcfb 22949 uffixfr 23427 plycpn 25802 insiga 33135 dfon2lem8 34762 trintALTVD 43641 trintALT 43642 elintd 43763 intsaluni 45045 intsal 45046 |
Copyright terms: Public domain | W3C validator |