Theorem elrab3 3630

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 3629	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
3	2	baib 540	1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433

This theorem is referenced by:  unimax  4875  fnelfp  7119  fnelnfp  7121  fnse  8073  fin23lem30  10255  isf32lem5  10270  negn0  11570  ublbneg  12874  supminf  12876  sadval  16416  smuval  16441  dvdslcm  16558  dvdslcmf  16591  isprm2lem  16641  isacs1i  17614  isinito  17954  istermo  17955  subgacs  19127  nsgacs  19128  odngen  19543  sdrgacs  20773  lssacs  20957  mretopd  23075  txkgen  23635  xkoco1cn  23640  xkoco2cn  23641  xkoinjcn  23670  ordthmeolem  23784  shft2rab  25493  sca2rab  25497  lhop1lem  25998  ftalem5  27058  vmasum  27197  eqcuts2  27796  elmade  27867  addonbday  28289  israg  28783  ebtwntg  29069  eupth2lem3lem3  30318  eupth2lem3lem4  30319  eupth2lem3lem6  30321  cycpmco2lem1  33207  cycpmco2lem4  33210  cycpmco2  33214  ssdifidllem  33539  1arithufdlem2  33628  tgoldbachgt  34847  cvmliftmolem1  35509  neibastop3  36590  fdc  38112  pclvalN  40382  dvhb1dimN  41478  hdmaplkr  42405  aks4d1p8  42572  sticksstones1  42631  fsuppssind  43043  diophren  43258  islmodfg  43514  fsovcnvlem  44457  ntrneiel  44525  radcnvrat  44758  supminfxr  45907  stoweidlem34  46477