Theorem elrab3 3645

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440

This theorem is referenced by:  unimax  4898  fnelfp  7119  fnelnfp  7121  fnse  8073  fin23lem30  10250  isf32lem5  10265  negn0  11564  ublbneg  12844  supminf  12846  sadval  16381  smuval  16406  dvdslcm  16523  dvdslcmf  16556  isprm2lem  16606  isacs1i  17578  isinito  17918  istermo  17919  subgacs  19088  nsgacs  19089  odngen  19504  sdrgacs  20732  lssacs  20916  mretopd  23034  txkgen  23594  xkoco1cn  23599  xkoco2cn  23600  xkoinjcn  23629  ordthmeolem  23743  shft2rab  25463  sca2rab  25467  lhop1lem  25972  ftalem5  27041  vmasum  27181  eqscut2  27774  elmade  27839  israg  28718  ebtwntg  29004  eupth2lem3lem3  30254  eupth2lem3lem4  30255  eupth2lem3lem6  30257  cycpmco2lem1  33157  cycpmco2lem4  33160  cycpmco2  33164  ssdifidllem  33486  1arithufdlem2  33575  tgoldbachgt  34769  cvmliftmolem1  35424  neibastop3  36505  fdc  37885  pclvalN  40089  dvhb1dimN  41185  hdmaplkr  42112  aks4d1p8  42280  sticksstones1  42339  fsuppssind  42778  diophren  42997  islmodfg  43253  fsovcnvlem  44196  ntrneiel  44264  radcnvrat  44497  supminfxr  45650  stoweidlem34  46220