Theorem elrab3 3663

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452

This theorem is referenced by:  unimax  4911  fnelfp  7152  fnelnfp  7154  fnse  8115  fin23lem30  10302  isf32lem5  10317  negn0  11614  ublbneg  12899  supminf  12901  sadval  16433  smuval  16458  dvdslcm  16575  dvdslcmf  16608  isprm2lem  16658  isacs1i  17625  isinito  17965  istermo  17966  subgacs  19100  nsgacs  19101  odngen  19514  sdrgacs  20717  lssacs  20880  mretopd  22986  txkgen  23546  xkoco1cn  23551  xkoco2cn  23552  xkoinjcn  23581  ordthmeolem  23695  shft2rab  25416  sca2rab  25420  lhop1lem  25925  ftalem5  26994  vmasum  27134  eqscut2  27725  elmade  27786  israg  28631  ebtwntg  28916  eupth2lem3lem3  30166  eupth2lem3lem4  30167  eupth2lem3lem6  30169  cycpmco2lem1  33090  cycpmco2lem4  33093  cycpmco2  33097  ssdifidllem  33434  1arithufdlem2  33523  tgoldbachgt  34661  cvmliftmolem1  35275  neibastop3  36357  fdc  37746  pclvalN  39891  dvhb1dimN  40987  hdmaplkr  41914  aks4d1p8  42082  sticksstones1  42141  fsuppssind  42588  diophren  42808  islmodfg  43065  fsovcnvlem  44009  ntrneiel  44077  radcnvrat  44310  supminfxr  45467  stoweidlem34  46039