ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elrabi GIF version

Theorem elrabi 2905
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
Assertion
Ref Expression
elrabi (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrabi
StepHypRef Expression
1 clelab 2315 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2252 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 465 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 383 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1609 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 121 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2477 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 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