Theorem elrab3 3685

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477

This theorem is referenced by:  unimax  4949  fnelfp  7173  fnelnfp  7175  fnse  8119  fin23lem30  10337  isf32lem5  10352  negn0  11643  ublbneg  12917  supminf  12919  sadval  16397  smuval  16422  dvdslcm  16535  dvdslcmf  16568  isprm2lem  16618  isacs1i  17601  isinito  17946  istermo  17947  subgacs  19041  nsgacs  19042  odngen  19445  sdrgacs  20417  lssacs  20578  mretopd  22596  txkgen  23156  xkoco1cn  23161  xkoco2cn  23162  xkoinjcn  23191  ordthmeolem  23305  shft2rab  25025  sca2rab  25029  lhop1lem  25530  ftalem5  26581  vmasum  26719  eqscut2  27307  elmade  27362  israg  27948  ebtwntg  28240  eupth2lem3lem3  29483  eupth2lem3lem4  29484  eupth2lem3lem6  29486  cycpmco2lem1  32285  cycpmco2lem4  32288  cycpmco2  32292  tgoldbachgt  33675  cvmliftmolem1  34272  neibastop3  35247  fdc  36613  pclvalN  38761  dvhb1dimN  39857  hdmaplkr  40784  aks4d1p8  40952  sticksstones1  40962  fsuppssind  41165  diophren  41551  islmodfg  41811  fsovcnvlem  42764  ntrneiel  42832  radcnvrat  43073  supminfxr  44174  stoweidlem34  44750