Theorem elrab3 3629

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

Step	Hyp	Ref	Expression
1		elrab.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	elrab 3628	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
3	2	baib 539	1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443

This theorem is referenced by:  unimax  4836  fnelfp  6914  fnelnfp  6916  fnse  7810  fin23lem30  9753  isf32lem5  9768  negn0  11058  ublbneg  12321  supminf  12323  sadval  15795  smuval  15820  dvdslcm  15932  dvdslcmf  15965  isprm2lem  16015  isacs1i  16920  isinito  17252  istermo  17253  subgacs  18305  nsgacs  18306  odngen  18694  sdrgacs  19573  lssacs  19732  mretopd  21697  txkgen  22257  xkoco1cn  22262  xkoco2cn  22263  xkoinjcn  22292  ordthmeolem  22406  shft2rab  24112  sca2rab  24116  lhop1lem  24616  ftalem5  25662  vmasum  25800  israg  26491  ebtwntg  26776  eupth2lem3lem3  28015  eupth2lem3lem4  28016  eupth2lem3lem6  28018  cycpmco2lem1  30818  cycpmco2lem4  30821  cycpmco2  30825  tgoldbachgt  32044  cvmliftmolem1  32641  neibastop3  33823  fdc  35183  pclvalN  37186  dvhb1dimN  38282  hdmaplkr  39209  fsuppssind  39459  diophren  39754  islmodfg  40013  fsovcnvlem  40714  ntrneiel  40784  radcnvrat  41018  supminfxr  42103  stoweidlem34  42676