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  17594  isinito  17934  istermo  17935  subgacs  19069  nsgacs  19070  odngen  19483  sdrgacs  20686  lssacs  20849  mretopd  22955  txkgen  23515  xkoco1cn  23520  xkoco2cn  23521  xkoinjcn  23550  ordthmeolem  23664  shft2rab  25385  sca2rab  25389  lhop1lem  25894  ftalem5  26963  vmasum  27103  eqscut2  27694  elmade  27755  israg  28600  ebtwntg  28885  eupth2lem3lem3  30132  eupth2lem3lem4  30133  eupth2lem3lem6  30135  cycpmco2lem1  33056  cycpmco2lem4  33059  cycpmco2  33063  ssdifidllem  33400  1arithufdlem2  33489  tgoldbachgt  34627  cvmliftmolem1  35241  neibastop3  36323  fdc  37712  pclvalN  39857  dvhb1dimN  40953  hdmaplkr  41880  aks4d1p8  42048  sticksstones1  42107  fsuppssind  42554  diophren  42774  islmodfg  43031  fsovcnvlem  43975  ntrneiel  44043  radcnvrat  44276  supminfxr  45433  stoweidlem34  46005