Theorem elrab3 3645

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  unimax  4904  fnelfp  7184  fnelnfp  7186  fnse  8156  fin23lem30  10427  isf32lem5  10442  negn0  11752  ublbneg  13067  supminf  13069  sadval  16635  smuval  16660  dvdslcm  16782  dvdslcmf  16815  isprm2lem  16865  isacs1i  17840  isinito  18180  istermo  18181  subgacs  19380  nsgacs  19381  odngen  19800  sdrgacs  21067  lssacs  21251  ssdifidllem  21649  mretopd  23419  txkgen  23980  xkoco1cn  23985  xkoco2cn  23986  xkoinjcn  24015  ordthmeolem  24129  shft2rab  25838  sca2rab  25842  lhop1lem  26342  ftalem5  27413  vmasum  27552  eqcuts2  28181  elmade  28252  addonbday  28674  israg  29181  ebtwntg  29569  eupth2lem3lem3  30840  eupth2lem3lem4  30841  eupth2lem3lem6  30843  cycpmco2lem1  33737  cycpmco2lem4  33740  cycpmco2  33744  1arithufdlem2  34127  tgoldbachgt  35342  cvmliftmolem1  36136  onprcr  36552  nmulr0  37040  neibastop3  37246  fdc  38788  pclvalN  41056  dvhb1dimN  42152  hdmaplkr  43079  aks4d1p8  43246  sticksstones1  43305  fsuppssind  43730  diophren  43929  islmodfg  44180  fsovcnvlem  45122  ntrneiel  45190  radcnvrat  45407  supminfxr  46582  stoweidlem34  47152