Theorem elrab3 3618

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424

This theorem is referenced by:  unimax  4874  fnelfp  7029  fnelnfp  7031  fnse  7945  fin23lem30  10029  isf32lem5  10044  negn0  11334  ublbneg  12602  supminf  12604  sadval  16091  smuval  16116  dvdslcm  16231  dvdslcmf  16264  isprm2lem  16314  isacs1i  17283  isinito  17627  istermo  17628  subgacs  18704  nsgacs  18705  odngen  19097  sdrgacs  19984  lssacs  20144  mretopd  22151  txkgen  22711  xkoco1cn  22716  xkoco2cn  22717  xkoinjcn  22746  ordthmeolem  22860  shft2rab  24577  sca2rab  24581  lhop1lem  25082  ftalem5  26131  vmasum  26269  israg  26962  ebtwntg  27253  eupth2lem3lem3  28495  eupth2lem3lem4  28496  eupth2lem3lem6  28498  cycpmco2lem1  31295  cycpmco2lem4  31298  cycpmco2  31302  tgoldbachgt  32543  cvmliftmolem1  33143  eqscut2  33927  elmade  33978  neibastop3  34478  fdc  35830  pclvalN  37831  dvhb1dimN  38927  hdmaplkr  39854  aks4d1p8  40023  sticksstones1  40030  fsuppssind  40205  diophren  40551  islmodfg  40810  fsovcnvlem  41510  ntrneiel  41580  radcnvrat  41821  supminfxr  42894  stoweidlem34  43465