Theorem elrab3 3680

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496

This theorem is referenced by:  unimax  4866  fnelfp  6931  fnelnfp  6933  fnse  7821  fin23lem30  9758  isf32lem5  9773  negn0  11063  ublbneg  12327  supminf  12329  sadval  15799  smuval  15824  dvdslcm  15936  dvdslcmf  15969  isprm2lem  16019  isacs1i  16922  isinito  17254  istermo  17255  subgacs  18307  nsgacs  18308  odngen  18696  sdrgacs  19574  lssacs  19733  mretopd  21694  txkgen  22254  xkoco1cn  22259  xkoco2cn  22260  xkoinjcn  22289  ordthmeolem  22403  shft2rab  24103  sca2rab  24107  lhop1lem  24604  ftalem5  25648  vmasum  25786  israg  26477  ebtwntg  26762  eupth2lem3lem3  28003  eupth2lem3lem4  28004  eupth2lem3lem6  28006  cycpmco2lem1  30763  cycpmco2lem4  30766  cycpmco2  30770  tgoldbachgt  31929  cvmliftmolem1  32523  neibastop3  33705  fdc  35014  pclvalN  37020  dvhb1dimN  38116  hdmaplkr  39043  diophren  39403  islmodfg  39662  fsovcnvlem  40352  ntrneiel  40424  radcnvrat  40639  supminfxr  41733  stoweidlem34  42313