Theorem elrab3 3635

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431

This theorem is referenced by:  unimax  4887  fnelfp  7130  fnelnfp  7132  fnse  8083  fin23lem30  10264  isf32lem5  10279  negn0  11579  ublbneg  12883  supminf  12885  sadval  16425  smuval  16450  dvdslcm  16567  dvdslcmf  16600  isprm2lem  16650  isacs1i  17623  isinito  17963  istermo  17964  subgacs  19136  nsgacs  19137  odngen  19552  sdrgacs  20778  lssacs  20962  mretopd  23057  txkgen  23617  xkoco1cn  23622  xkoco2cn  23623  xkoinjcn  23652  ordthmeolem  23766  shft2rab  25475  sca2rab  25479  lhop1lem  25980  ftalem5  27040  vmasum  27179  eqcuts2  27778  elmade  27849  addonbday  28271  israg  28765  ebtwntg  29051  eupth2lem3lem3  30300  eupth2lem3lem4  30301  eupth2lem3lem6  30303  cycpmco2lem1  33187  cycpmco2lem4  33190  cycpmco2  33194  ssdifidllem  33516  1arithufdlem2  33605  tgoldbachgt  34807  cvmliftmolem1  35463  neibastop3  36544  fdc  38066  pclvalN  40336  dvhb1dimN  41432  hdmaplkr  42359  aks4d1p8  42526  sticksstones1  42585  fsuppssind  43026  diophren  43241  islmodfg  43497  fsovcnvlem  44440  ntrneiel  44508  radcnvrat  44741  supminfxr  45892  stoweidlem34  46462