Theorem elrab3 3657

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446

This theorem is referenced by:  unimax  4904  fnelfp  7131  fnelnfp  7133  fnse  8089  fin23lem30  10271  isf32lem5  10286  negn0  11583  ublbneg  12868  supminf  12870  sadval  16402  smuval  16427  dvdslcm  16544  dvdslcmf  16577  isprm2lem  16627  isacs1i  17598  isinito  17938  istermo  17939  subgacs  19075  nsgacs  19076  odngen  19491  sdrgacs  20721  lssacs  20905  mretopd  23012  txkgen  23572  xkoco1cn  23577  xkoco2cn  23578  xkoinjcn  23607  ordthmeolem  23721  shft2rab  25442  sca2rab  25446  lhop1lem  25951  ftalem5  27020  vmasum  27160  eqscut2  27752  elmade  27816  israg  28677  ebtwntg  28962  eupth2lem3lem3  30209  eupth2lem3lem4  30210  eupth2lem3lem6  30212  cycpmco2lem1  33098  cycpmco2lem4  33101  cycpmco2  33105  ssdifidllem  33420  1arithufdlem2  33509  tgoldbachgt  34647  cvmliftmolem1  35261  neibastop3  36343  fdc  37732  pclvalN  39877  dvhb1dimN  40973  hdmaplkr  41900  aks4d1p8  42068  sticksstones1  42127  fsuppssind  42574  diophren  42794  islmodfg  43051  fsovcnvlem  43995  ntrneiel  44063  radcnvrat  44296  supminfxr  45453  stoweidlem34  46025