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

Theorem elrab3 2751
 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 2750 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
32baib 862 1 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103   = wceq 1285   ∈ wcel 1434  {crab 2353 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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rab 2358  df-v 2604 This theorem is referenced by:  unimax  3643  frind  4115  ordtriexmidlem2  4272  ordtriexmid  4273  ordtri2orexmid  4274  onsucelsucexmid  4281  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4322  acexmidlema  5534  acexmidlemb  5535  isnumi  6510  genpelvl  6764  genpelvu  6765  cauappcvgprlemladdru  6908  cauappcvgprlem1  6911  caucvgprlem1  6931  supinfneg  8764  infsupneg  8765  supminfex  8766  ublbneg  8779  negm  8781  sizeinfuni  9801  infssuzex  10489  gcddvds  10499  dvdslegcd  10500  bezoutlemsup  10542  lcmval  10589  dvdslcm  10595  isprm2lem  10642
 Copyright terms: Public domain W3C validator