| Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > elinintab | Structured version Visualization version GIF version | ||
| Description: Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
| Ref | Expression |
|---|---|
| elinintab | ⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elin 3922 | . 2 ⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ ∩ {𝑥 ∣ 𝜑})) | |
| 2 | elintabg 4925 | . . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | |
| 3 | 2 | pm5.32i 585 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) |
| 4 | 1, 3 | bitri 278 | 1 ⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∀wal 1568 ∈ wcel 2146 {cab 2743 ∩ cin 3905 ∩ cint 4914 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-tru 1573 df-ex 1813 df-nf 1817 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3082 df-v 3459 df-in 3913 df-int 4915 |
| This theorem is used by: inintabss 44362 inintabd 44363 elcnvcnvintab 44366 |
| Copyright terms: Public domain | W3C validator |