![]() |
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 |
---|---|
inteqab.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
elintab | ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inteqab.1 | . . 3 ⊢ 𝐴 ∈ V | |
2 | 1 | elint 4782 | . 2 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦)) |
3 | nfsab1 2782 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
4 | nfv 1890 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
5 | 3, 4 | nfim 1876 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) |
6 | nfv 1890 | . . 3 ⊢ Ⅎ𝑦(𝜑 → 𝐴 ∈ 𝑥) | |
7 | eleq1w 2863 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
8 | abid 2777 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
9 | 7, 8 | syl6bb 288 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
10 | eleq2w 2864 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
11 | 9, 10 | imbi12d 346 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ (𝜑 → 𝐴 ∈ 𝑥))) |
12 | 5, 6, 11 | cbvalv1 2318 | . 2 ⊢ (∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
13 | 2, 12 | bitri 276 | 1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1518 ∈ wcel 2079 {cab 2773 Vcvv 3432 ∩ cint 4776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-int 4777 |
This theorem is referenced by: elintrab 4788 intmin4 4805 intab 4806 intid 5235 dfom3 8945 dfom5 8948 tc2 9019 dfnn2 11488 brintclab 14183 efgi 18560 efgi2 18566 mclsax 32369 heibor1lem 34565 intabssd 39321 elmapintab 39392 cotrintab 39410 dffrege76 39721 |
Copyright terms: Public domain | W3C validator |