Theorem elrab3 3647

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442

This theorem is referenced by:  unimax  4900  fnelfp  7121  fnelnfp  7123  fnse  8075  fin23lem30  10252  isf32lem5  10267  negn0  11566  ublbneg  12846  supminf  12848  sadval  16383  smuval  16408  dvdslcm  16525  dvdslcmf  16558  isprm2lem  16608  isacs1i  17580  isinito  17920  istermo  17921  subgacs  19090  nsgacs  19091  odngen  19506  sdrgacs  20734  lssacs  20918  mretopd  23036  txkgen  23596  xkoco1cn  23601  xkoco2cn  23602  xkoinjcn  23631  ordthmeolem  23745  shft2rab  25465  sca2rab  25469  lhop1lem  25974  ftalem5  27043  vmasum  27183  eqcuts2  27782  elmade  27853  addonbday  28275  israg  28769  ebtwntg  29055  eupth2lem3lem3  30305  eupth2lem3lem4  30306  eupth2lem3lem6  30308  cycpmco2lem1  33208  cycpmco2lem4  33211  cycpmco2  33215  ssdifidllem  33537  1arithufdlem2  33626  tgoldbachgt  34820  cvmliftmolem1  35475  neibastop3  36556  fdc  37946  pclvalN  40150  dvhb1dimN  41246  hdmaplkr  42173  aks4d1p8  42341  sticksstones1  42400  fsuppssind  42836  diophren  43055  islmodfg  43311  fsovcnvlem  44254  ntrneiel  44322  radcnvrat  44555  supminfxr  45708  stoweidlem34  46278