![]() |
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 2315 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑))) | |
2 | eleq1 2252 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉)) | |
3 | 2 | anbi1d 465 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝑉 ∧ 𝜑) ↔ (𝐴 ∈ 𝑉 ∧ 𝜑))) |
4 | 3 | simprbda 383 | . . . 4 ⊢ ((𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
5 | 4 | exlimiv 1609 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ (𝑥 ∈ 𝑉 ∧ 𝜑)) → 𝐴 ∈ 𝑉) |
6 | 1, 5 | sylbi 121 | . 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉) |
7 | df-rab 2477 | . 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} | |
8 | 6, 7 | eleq2s 2284 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 ∃wex 1503 ∈ wcel 2160 {cab 2175 {crab 2472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-rab 2477 |
This theorem is referenced by: ordtriexmidlem 4536 ordtri2or2exmidlem 4543 onsucelsucexmidlem 4546 ordsoexmid 4579 reg3exmidlemwe 4596 elfvmptrab1 5631 acexmidlemcase 5891 ssfirab 6962 exmidonfinlem 7222 cc4f 7298 genpelvl 7541 genpelvu 7542 suplocsrlempr 7836 nnindnn 7922 sup3exmid 8944 nnind 8965 supinfneg 9625 infsupneg 9626 supminfex 9627 ublbneg 9643 hashinfuni 10789 zsupcllemstep 11978 infssuzex 11982 infssuzledc 11983 bezoutlemsup 12042 uzwodc 12070 lcmgcdlem 12109 phisum 12272 oddennn 12443 evenennn 12444 znnen 12449 ennnfonelemg 12454 psrbagf 13948 txdis1cn 14238 reopnap 14498 divcnap 14515 limccl 14588 dvlemap 14609 dvaddxxbr 14625 dvmulxxbr 14626 dvcoapbr 14631 dvcjbr 14632 dvrecap 14637 dveflem 14647 |
Copyright terms: Public domain | W3C validator |