![]() |
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 4615 | . 2 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦)) |
3 | nfsab1 2760 | . . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑} | |
4 | nfv 1994 | . . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦 | |
5 | 3, 4 | nfim 1976 | . . 3 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) |
6 | nfv 1994 | . . 3 ⊢ Ⅎ𝑦(𝜑 → 𝐴 ∈ 𝑥) | |
7 | eleq1w 2832 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑})) | |
8 | abid 2758 | . . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
9 | 7, 8 | syl6bb 276 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)) |
10 | eleq2w 2833 | . . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥)) | |
11 | 9, 10 | imbi12d 333 | . . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ (𝜑 → 𝐴 ∈ 𝑥))) |
12 | 5, 6, 11 | cbval 2431 | . 2 ⊢ (∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
13 | 2, 12 | bitri 264 | 1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wal 1628 ∈ wcel 2144 {cab 2756 Vcvv 3349 ∩ cint 4609 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-v 3351 df-int 4610 |
This theorem is referenced by: elintrab 4621 intmin4 4638 intab 4639 intid 5054 dfom3 8707 dfom5 8710 tc2 8781 dfnn2 11234 brintclab 13949 efgi 18338 efgi2 18344 mclsax 31798 heibor1lem 33933 elmapintab 38421 intabssd 38435 cotrintab 38440 dffrege76 38752 |
Copyright terms: Public domain | W3C validator |