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

Theorem elrabi 2883
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 2296 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2233 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 462 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 381 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1591 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 120 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2457 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2265 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1348  wex 1485  wcel 2141  {cab 2156  {crab 2452
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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-rab 2457
This theorem is referenced by:  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  ordsoexmid  4546  reg3exmidlemwe  4563  elfvmptrab1  5590  acexmidlemcase  5848  ssfirab  6911  exmidonfinlem  7170  cc4f  7231  genpelvl  7474  genpelvu  7475  suplocsrlempr  7769  nnindnn  7855  sup3exmid  8873  nnind  8894  supinfneg  9554  infsupneg  9555  supminfex  9556  ublbneg  9572  hashinfuni  10711  zsupcllemstep  11900  infssuzex  11904  infssuzledc  11905  bezoutlemsup  11964  uzwodc  11992  lcmgcdlem  12031  phisum  12194  oddennn  12347  evenennn  12348  znnen  12353  ennnfonelemg  12358  txdis1cn  13072  reopnap  13332  divcnap  13349  limccl  13422  dvlemap  13443  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481
  Copyright terms: Public domain W3C validator