Theorem elrab3 3646

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  unimax  4905  fnelfp  7173  fnelnfp  7175  fnse  8131  fin23lem30  10344  isf32lem5  10359  negn0  11667  ublbneg  12982  supminf  12984  sadval  16546  smuval  16571  dvdslcm  16688  dvdslcmf  16721  isprm2lem  16771  isacs1i  17745  isinito  18085  istermo  18086  subgacs  19284  nsgacs  19285  odngen  19704  sdrgacs  20967  lssacs  21151  ssdifidllem  21547  mretopd  23317  txkgen  23878  xkoco1cn  23883  xkoco2cn  23884  xkoinjcn  23913  ordthmeolem  24027  shft2rab  25736  sca2rab  25740  lhop1lem  26240  ftalem5  27313  vmasum  27452  eqcuts2  28051  elmade  28122  addonbday  28544  israg  29051  ebtwntg  29439  eupth2lem3lem3  30710  eupth2lem3lem4  30711  eupth2lem3lem6  30713  cycpmco2lem1  33566  cycpmco2lem4  33569  cycpmco2  33573  1arithufdlem2  33955  tgoldbachgt  35171  cvmliftmolem1  35860  nmulr0  36775  neibastop3  36981  fdc  38495  pclvalN  40763  dvhb1dimN  41859  hdmaplkr  42786  aks4d1p8  42953  sticksstones1  43012  fsuppssind  43439  diophren  43654  islmodfg  43910  fsovcnvlem  44853  ntrneiel  44921  radcnvrat  45138  supminfxr  46292  stoweidlem34  46862