| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elint2 | Structured version Visualization version GIF version | ||
| Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999.) |
| Ref | Expression |
|---|---|
| elint2.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| elint2 | ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elint2.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 2 | 1 | elint 4952 | . 2 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) |
| 3 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥)) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∩ 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: int0 4962 ssint 4964 intssuni 4970 iinuni 5098 onint 7810 intwun 10775 inttsk 10814 intgru 10854 subgint 19168 subrngint 20560 subrgint 20595 lssintcl 20962 toponmre 23101 alexsubALTlem3 24057 shintcli 31348 chintcli 31350 intlidl 33448 fin2so 37614 intidl 38036 mzpincl 42745 elimaint 43662 elintima 43666 intsal 46345 salgencntex 46358 |
| Copyright terms: Public domain | W3C validator |