Theorem elrab3 3649

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444

This theorem is referenced by:  unimax  4902  fnelfp  7133  fnelnfp  7135  fnse  8087  fin23lem30  10266  isf32lem5  10281  negn0  11580  ublbneg  12860  supminf  12862  sadval  16397  smuval  16422  dvdslcm  16539  dvdslcmf  16572  isprm2lem  16622  isacs1i  17594  isinito  17934  istermo  17935  subgacs  19107  nsgacs  19108  odngen  19523  sdrgacs  20751  lssacs  20935  mretopd  23053  txkgen  23613  xkoco1cn  23618  xkoco2cn  23619  xkoinjcn  23648  ordthmeolem  23762  shft2rab  25482  sca2rab  25486  lhop1lem  25991  ftalem5  27060  vmasum  27200  eqcuts2  27799  elmade  27870  addonbday  28292  israg  28787  ebtwntg  29073  eupth2lem3lem3  30323  eupth2lem3lem4  30324  eupth2lem3lem6  30326  cycpmco2lem1  33226  cycpmco2lem4  33229  cycpmco2  33233  ssdifidllem  33555  1arithufdlem2  33644  tgoldbachgt  34847  cvmliftmolem1  35503  neibastop3  36584  fdc  38025  pclvalN  40295  dvhb1dimN  41391  hdmaplkr  42318  aks4d1p8  42486  sticksstones1  42545  fsuppssind  42980  diophren  43199  islmodfg  43455  fsovcnvlem  44398  ntrneiel  44466  radcnvrat  44699  supminfxr  45851  stoweidlem34  46421