| 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 2829 | . . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) | |
| 2 | 1 | ralbidv 3178 | . 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
| 3 | dfint2 4948 | . 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥} | |
| 4 | 2, 3 | elab2g 3680 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∩ cint 4946 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-int 4947 |
| This theorem is referenced by: elinti 4955 elintabg 4957 elrint 4989 onmindif 6476 onmindif2 7827 mremre 17647 toponmre 23101 1stcfb 23453 uffixfr 23931 plycpn 26331 insiga 34138 dfon2lem8 35791 trintALTVD 44900 trintALT 44901 elintd 45079 intsaluni 46344 intsal 46345 |
| Copyright terms: Public domain | W3C validator |