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

Theorem elrabi 2837
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 2265 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2202 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 460 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 380 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1577 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 120 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2425 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2234 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1331  wex 1468  wcel 1480  {cab 2125  {crab 2420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-rab 2425
This theorem is referenced by:  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  ordsoexmid  4477  reg3exmidlemwe  4493  elfvmptrab1  5515  acexmidlemcase  5769  ssfirab  6822  exmidonfinlem  7054  cc4f  7089  genpelvl  7332  genpelvu  7333  suplocsrlempr  7627  nnindnn  7713  sup3exmid  8727  nnind  8748  supinfneg  9402  infsupneg  9403  supminfex  9404  ublbneg  9417  hashinfuni  10535  zsupcllemstep  11649  infssuzex  11653  infssuzledc  11654  bezoutlemsup  11708  lcmgcdlem  11769  oddennn  11916  evenennn  11917  znnen  11922  ennnfonelemg  11927  txdis1cn  12461  reopnap  12721  divcnap  12738  limccl  12811  dvlemap  12832  dvaddxxbr  12848  dvmulxxbr  12849  dvcoapbr  12854  dvcjbr  12855  dvrecap  12860  dveflem  12870
  Copyright terms: Public domain W3C validator