![]() |
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 2826 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
2 | 1 | ralbidv 3173 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
3 | dfint2 4908 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
4 | 2, 3 | elab2g 3631 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ∀wral 3063 ∩ cint 4906 |
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 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3064 df-int 4907 |
This theorem is referenced by: elinti 4915 elintabg 4917 elrint 4951 onmindif 6406 onmindif2 7733 mremre 17420 toponmre 22372 1stcfb 22724 uffixfr 23202 plycpn 25577 insiga 32516 dfon2lem8 34159 trintALTVD 42963 trintALT 42964 elintd 43085 intsaluni 44361 intsal 44362 |
Copyright terms: Public domain | W3C validator |