![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elrabi | GIF version |
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
Ref | Expression |
---|---|
elrabi | ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clelab 2224 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑))) | |
2 | eleq1 2162 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉)) | |
3 | 2 | anbi1d 456 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑))) |
4 | 3 | simprbda 378 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
5 | 4 | exlimiv 1545 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
6 | 1, 5 | sylbi 120 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉) |
7 | df-rab 2384 | . 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} | |
8 | 6, 7 | eleq2s 2194 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1299 ∃wex 1436 ∈ wcel 1448 {cab 2086 {crab 2379 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-rab 2384 |
This theorem is referenced by: ordtriexmidlem 4373 ordtri2or2exmidlem 4379 onsucelsucexmidlem 4382 ordsoexmid 4415 reg3exmidlemwe 4431 elfvmptrab1 5447 acexmidlemcase 5701 ssfirab 6750 ctssdclemr 6911 genpelvl 7221 genpelvu 7222 nnindnn 7578 sup3exmid 8573 nnind 8594 supinfneg 9240 infsupneg 9241 supminfex 9242 ublbneg 9255 hashinfuni 10364 zsupcllemstep 11433 infssuzex 11437 infssuzledc 11438 bezoutlemsup 11490 lcmgcdlem 11551 oddennn 11697 evenennn 11698 znnen 11703 ennnfonelemg 11708 txdis1cn 12228 limccl 12510 dvlemap 12522 |
Copyright terms: Public domain | W3C validator |