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 1540   ∈ wcel 2109  {crab 3394

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 3395  df-v 3438

This theorem is referenced by:  unimax  4894  fnelfp  7111  fnelnfp  7113  fnse  8066  fin23lem30  10236  isf32lem5  10251  negn0  11549  ublbneg  12834  supminf  12836  sadval  16367  smuval  16392  dvdslcm  16509  dvdslcmf  16542  isprm2lem  16592  isacs1i  17563  isinito  17903  istermo  17904  subgacs  19040  nsgacs  19041  odngen  19456  sdrgacs  20686  lssacs  20870  mretopd  22977  txkgen  23537  xkoco1cn  23542  xkoco2cn  23543  xkoinjcn  23572  ordthmeolem  23686  shft2rab  25407  sca2rab  25411  lhop1lem  25916  ftalem5  26985  vmasum  27125  eqscut2  27717  elmade  27781  israg  28642  ebtwntg  28927  eupth2lem3lem3  30174  eupth2lem3lem4  30175  eupth2lem3lem6  30177  cycpmco2lem1  33068  cycpmco2lem4  33071  cycpmco2  33075  ssdifidllem  33393  1arithufdlem2  33482  tgoldbachgt  34631  cvmliftmolem1  35254  neibastop3  36336  fdc  37725  pclvalN  39869  dvhb1dimN  40965  hdmaplkr  41892  aks4d1p8  42060  sticksstones1  42119  fsuppssind  42566  diophren  42786  islmodfg  43042  fsovcnvlem  43986  ntrneiel  44054  radcnvrat  44287  supminfxr  45443  stoweidlem34  46015