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

Theorem elrab3 2869
 Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)
Hypothesis
Ref Expression
elrab.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elrab3 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab3
StepHypRef Expression
1 elrab.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
21elrab 2868 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
32baib 905 1 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1335   ∈ wcel 2128  {crab 2439 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-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-v 2714 This theorem is referenced by:  unimax  3806  undifexmid  4154  frind  4312  ordtriexmidlem2  4478  ordtriexmid  4479  ontriexmidim  4480  ordtri2orexmid  4481  onsucelsucexmid  4488  0elsucexmid  4523  ordpwsucexmid  4528  ordtri2or2exmid  4529  ontri2orexmidim  4530  canth  5775  acexmidlema  5812  acexmidlemb  5813  isnumi  7111  genpelvl  7426  genpelvu  7427  cauappcvgprlemladdru  7570  cauappcvgprlem1  7573  caucvgprlem1  7593  sup3exmid  8822  supinfneg  9500  infsupneg  9501  supminfex  9502  ublbneg  9515  negm  9517  hashinfuni  10644  infssuzex  11828  gcddvds  11838  dvdslegcd  11839  bezoutlemsup  11884  lcmval  11931  dvdslcm  11937  isprm2lem  11984
 Copyright terms: Public domain W3C validator