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  7131  fnelnfp  7133  fnse  8085  fin23lem30  10264  isf32lem5  10279  negn0  11578  ublbneg  12858  supminf  12860  sadval  16395  smuval  16420  dvdslcm  16537  dvdslcmf  16570  isprm2lem  16620  isacs1i  17592  isinito  17932  istermo  17933  subgacs  19102  nsgacs  19103  odngen  19518  sdrgacs  20746  lssacs  20930  mretopd  23048  txkgen  23608  xkoco1cn  23613  xkoco2cn  23614  xkoinjcn  23643  ordthmeolem  23757  shft2rab  25477  sca2rab  25481  lhop1lem  25986  ftalem5  27055  vmasum  27195  eqcuts2  27794  elmade  27865  addonbday  28287  israg  28781  ebtwntg  29067  eupth2lem3lem3  30317  eupth2lem3lem4  30318  eupth2lem3lem6  30320  cycpmco2lem1  33220  cycpmco2lem4  33223  cycpmco2  33227  ssdifidllem  33549  1arithufdlem2  33638  tgoldbachgt  34841  cvmliftmolem1  35497  neibastop3  36578  fdc  37996  pclvalN  40266  dvhb1dimN  41362  hdmaplkr  42289  aks4d1p8  42457  sticksstones1  42516  fsuppssind  42951  diophren  43170  islmodfg  43426  fsovcnvlem  44369  ntrneiel  44437  radcnvrat  44670  supminfxr  45822  stoweidlem34  46392