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

Theorem elrab3 3685
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 3684 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
32baib 536 1 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wcel 2107  {crab 3147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502
This theorem is referenced by:  unimax  4872  fnelfp  6935  fnelnfp  6937  fnse  7823  fin23lem30  9758  isf32lem5  9773  negn0  11063  ublbneg  12327  supminf  12329  sadval  15800  smuval  15825  dvdslcm  15937  dvdslcmf  15970  isprm2lem  16020  isacs1i  16923  isinito  17255  istermo  17256  subgacs  18258  nsgacs  18259  odngen  18638  sdrgacs  19516  lssacs  19675  mretopd  21635  txkgen  22195  xkoco1cn  22200  xkoco2cn  22201  xkoinjcn  22230  ordthmeolem  22344  shft2rab  24043  sca2rab  24047  lhop1lem  24544  ftalem5  25587  vmasum  25725  israg  26416  ebtwntg  26701  eupth2lem3lem3  27942  eupth2lem3lem4  27943  eupth2lem3lem6  27945  cycpmco2lem1  30701  cycpmco2lem4  30704  cycpmco2  30708  tgoldbachgt  31839  cvmliftmolem1  32431  neibastop3  33613  fdc  34907  pclvalN  36912  dvhb1dimN  38008  hdmaplkr  38935  diophren  39294  islmodfg  39553  fsovcnvlem  40243  ntrneiel  40315  radcnvrat  40530  supminfxr  41624  stoweidlem34  42204
  Copyright terms: Public domain W3C validator