MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrab3 Structured version   Visualization version   GIF version

Theorem elrab3 3351
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 3350 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
32baib 943 1 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987  {crab 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191
This theorem is referenced by:  unimax  4444  fnelfp  6401  fnelnfp  6403  fnse  7246  fin23lem30  9115  isf32lem5  9130  negn0  10410  ublbneg  11724  supminf  11726  sadval  15109  smuval  15134  dvdslcm  15242  dvdslcmf  15275  isacs1i  16246  isinito  16578  istermo  16579  subgacs  17557  nsgacs  17558  odngen  17920  lssacs  18895  mretopd  20815  txkgen  21374  xkoco1cn  21379  xkoco2cn  21380  xkoinjcn  21409  ordthmeolem  21523  shft2rab  23195  sca2rab  23199  lhop1lem  23693  ftalem5  24716  vmasum  24854  israg  25505  ebtwntg  25775  eupth2lem3lem3  26969  eupth2lem3lem4  26970  eupth2lem3lem6  26972  cvmliftmolem1  30998  nobndlem5  31586  nobndup  31590  nobnddown  31591  neibastop3  32026  fdc  33200  pclvalN  34683  dvhb1dimN  35781  hdmaplkr  36712  diophren  36884  islmodfg  37146  sdrgacs  37279  fsovcnvlem  37816  ntrneiel  37888  radcnvrat  38022  stoweidlem34  39579
  Copyright terms: Public domain W3C validator