![]() |
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 2207 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑))) | |
2 | eleq1 2145 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉)) | |
3 | 2 | anbi1d 453 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑))) |
4 | 3 | simprbda 375 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
5 | 4 | exlimiv 1530 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
6 | 1, 5 | sylbi 119 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉) |
7 | df-rab 2362 | . 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} | |
8 | 6, 7 | eleq2s 2177 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 = wceq 1285 ∃wex 1422 ∈ wcel 1434 {cab 2069 {crab 2357 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-11 1438 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-rab 2362 |
This theorem is referenced by: ordtriexmidlem 4291 ordtri2or2exmidlem 4297 onsucelsucexmidlem 4300 ordsoexmid 4333 reg3exmidlemwe 4349 acexmidlemcase 5558 ssfirab 6475 genpelvl 6816 genpelvu 6817 nnindnn 7173 nnind 8174 supinfneg 8816 infsupneg 8817 supminfex 8818 ublbneg 8831 hashinfuni 9853 zsupcllemstep 10548 infssuzex 10552 infssuzledc 10553 bezoutlemsup 10605 lcmgcdlem 10666 oddennn 10812 evenennn 10813 znnen 10818 |
Copyright terms: Public domain | W3C validator |