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

Theorem elrabi 2790
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 2224 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2162 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 456 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 378 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1545 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 120 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2384 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2194 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1299  wex 1436  wcel 1448  {cab 2086  {crab 2379
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-rab 2384
This theorem is referenced by:  ordtriexmidlem  4373  ordtri2or2exmidlem  4379  onsucelsucexmidlem  4382  ordsoexmid  4415  reg3exmidlemwe  4431  elfvmptrab1  5447  acexmidlemcase  5701  ssfirab  6750  ctssdclemr  6911  genpelvl  7221  genpelvu  7222  nnindnn  7578  sup3exmid  8573  nnind  8594  supinfneg  9240  infsupneg  9241  supminfex  9242  ublbneg  9255  hashinfuni  10364  zsupcllemstep  11433  infssuzex  11437  infssuzledc  11438  bezoutlemsup  11490  lcmgcdlem  11551  oddennn  11697  evenennn  11698  znnen  11703  ennnfonelemg  11708  txdis1cn  12228  limccl  12510  dvlemap  12522
  Copyright terms: Public domain W3C validator