| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elintab | Structured version Visualization version GIF version | ||
| Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.) |
| Ref | Expression |
|---|---|
| elintab.ex | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| elintab | ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elintab.ex | . 2 ⊢ 𝐴 ∈ V | |
| 2 | elintabg 4957 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∈ wcel 2108 {cab 2714 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-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-int 4947 |
| This theorem is referenced by: elintrab 4960 intmin4 4977 intab 4978 intidOLD 5463 dfom3 9687 dfom5 9690 tc2 9782 dfnn2 12279 brintclab 15040 efgi 19737 efgi2 19743 dfn0s2 28336 mclsax 35574 heibor1lem 37816 intabssd 43532 elmapintab 43609 cotrintab 43627 dffrege76 43952 |
| Copyright terms: Public domain | W3C validator |