Theorem elrab3 3651

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456

This theorem is referenced by:  unimax  4903  fnelfp  7159  fnelnfp  7161  fnse  8113  fin23lem30  10299  isf32lem5  10314  negn0  11616  ublbneg  12934  supminf  12936  sadval  16490  smuval  16515  dvdslcm  16632  dvdslcmf  16665  isprm2lem  16715  isacs1i  17689  isinito  18029  istermo  18030  subgacs  19202  nsgacs  19203  odngen  19617  sdrgacs  20850  lssacs  21034  mretopd  23152  txkgen  23712  xkoco1cn  23717  xkoco2cn  23718  xkoinjcn  23747  ordthmeolem  23861  shft2rab  25570  sca2rab  25574  lhop1lem  26075  ftalem5  27141  vmasum  27280  eqcuts2  27879  elmade  27950  addonbday  28372  israg  28870  ebtwntg  29183  eupth2lem3lem3  30432  eupth2lem3lem4  30433  eupth2lem3lem6  30435  cycpmco2lem1  33306  cycpmco2lem4  33309  cycpmco2  33313  ssdifidllem  33643  1arithufdlem2  33741  tgoldbachgt  34957  cvmliftmolem1  35631  nmulr0  36545  neibastop3  36722  fdc  38244  pclvalN  40514  dvhb1dimN  41610  hdmaplkr  42537  aks4d1p8  42704  sticksstones1  42763  fsuppssind  43175  diophren  43390  islmodfg  43646  fsovcnvlem  44589  ntrneiel  44657  radcnvrat  44890  supminfxr  46038  stoweidlem34  46608