Theorem elrab3 3649

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456

This theorem is used by:  unimax  4910  fnelfp  7211  fnelnfp  7213  onprcr  7825  fnse  8187  fin23lem30  10459  isf32lem5  10474  negn0  11784  ublbneg  13100  supminf  13102  sadval  16670  smuval  16695  dvdslcm  16817  dvdslcmf  16850  isprm2lem  16900  isacs1i  17881  isinito  18221  istermo  18222  subgacs  19421  nsgacs  19422  odngen  19842  sdrgacs  21109  lssacs  21293  ssdifidllem  21691  mretopd  23465  txkgen  24026  xkoco1cn  24031  xkoco2cn  24032  xkoinjcn  24061  ordthmeolem  24175  shft2rab  25884  sca2rab  25888  lhop1lem  26388  ftalem5  27461  vmasum  27600  eqcuts2  28229  elmade  28300  addonbday  28722  israg  29229  ebtwntg  29617  eupth2lem3lem3  30888  eupth2lem3lem4  30889  eupth2lem3lem6  30891  cycpmco2lem1  33786  cycpmco2lem4  33789  cycpmco2  33793  1arithufdlem2  34181  tgoldbachgt  35403  cvmliftmolem1  36254  nmulr0  37159  neibastop3  37365  fdc  38945  pclvalN  41213  dvhb1dimN  42309  hdmaplkr  43236  aks4d1p8  43403  sticksstones1  43462  fsuppssind  43887  diophren  44086  islmodfg  44337  fsovcnvlem  45274  ntrneiel  45342  radcnvrat  45559  supminfxr  46747  stoweidlem34  47317