Theorem elrab3 3626

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435

This theorem is referenced by:  unimax  4878  fnelfp  7056  fnelnfp  7058  fnse  7983  fin23lem30  10107  isf32lem5  10122  negn0  11413  ublbneg  12682  supminf  12684  sadval  16172  smuval  16197  dvdslcm  16312  dvdslcmf  16345  isprm2lem  16395  isacs1i  17375  isinito  17720  istermo  17721  subgacs  18798  nsgacs  18799  odngen  19191  sdrgacs  20078  lssacs  20238  mretopd  22252  txkgen  22812  xkoco1cn  22817  xkoco2cn  22818  xkoinjcn  22847  ordthmeolem  22961  shft2rab  24681  sca2rab  24685  lhop1lem  25186  ftalem5  26235  vmasum  26373  israg  27067  ebtwntg  27359  eupth2lem3lem3  28603  eupth2lem3lem4  28604  eupth2lem3lem6  28606  cycpmco2lem1  31402  cycpmco2lem4  31405  cycpmco2  31409  tgoldbachgt  32652  cvmliftmolem1  33252  eqscut2  34009  elmade  34060  neibastop3  34560  fdc  35912  pclvalN  37911  dvhb1dimN  39007  hdmaplkr  39934  aks4d1p8  40102  sticksstones1  40109  fsuppssind  40289  diophren  40642  islmodfg  40901  fsovcnvlem  41628  ntrneiel  41698  radcnvrat  41939  supminfxr  43011  stoweidlem34  43582