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

Theorem elrabi 2754
 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 2207 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2145 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 453 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 375 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1530 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 119 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2362 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 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