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

Theorem elrab3 3680
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 3679 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
32baib 536 1 (𝐴𝐵 → (𝐴 ∈ {𝑥𝐵𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  {crab 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497
This theorem is referenced by:  unimax  4867  fnelfp  6930  fnelnfp  6932  fnse  7818  fin23lem30  9753  isf32lem5  9768  negn0  11058  ublbneg  12322  supminf  12324  sadval  15795  smuval  15820  dvdslcm  15932  dvdslcmf  15965  isprm2lem  16015  isacs1i  16918  isinito  17250  istermo  17251  subgacs  18253  nsgacs  18254  odngen  18633  sdrgacs  19511  lssacs  19670  mretopd  21630  txkgen  22190  xkoco1cn  22195  xkoco2cn  22196  xkoinjcn  22225  ordthmeolem  22339  shft2rab  24038  sca2rab  24042  lhop1lem  24539  ftalem5  25582  vmasum  25720  israg  26411  ebtwntg  26696  eupth2lem3lem3  27937  eupth2lem3lem4  27938  eupth2lem3lem6  27940  cycpmco2lem1  30696  cycpmco2lem4  30699  cycpmco2  30703  tgoldbachgt  31834  cvmliftmolem1  32426  neibastop3  33608  fdc  34903  pclvalN  36908  dvhb1dimN  38004  hdmaplkr  38931  diophren  39290  islmodfg  39549  fsovcnvlem  40239  ntrneiel  40311  radcnvrat  40526  supminfxr  41620  stoweidlem34  42200
  Copyright terms: Public domain W3C validator