Theorem elrab3 3683

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {crab 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498

This theorem is referenced by:  unimax  4876  fnelfp  6939  fnelnfp  6941  fnse  7829  fin23lem30  9766  isf32lem5  9781  negn0  11071  ublbneg  12336  supminf  12338  sadval  15807  smuval  15832  dvdslcm  15944  dvdslcmf  15977  isprm2lem  16027  isacs1i  16930  isinito  17262  istermo  17263  subgacs  18315  nsgacs  18316  odngen  18704  sdrgacs  19582  lssacs  19741  mretopd  21702  txkgen  22262  xkoco1cn  22267  xkoco2cn  22268  xkoinjcn  22297  ordthmeolem  22411  shft2rab  24111  sca2rab  24115  lhop1lem  24612  ftalem5  25656  vmasum  25794  israg  26485  ebtwntg  26770  eupth2lem3lem3  28011  eupth2lem3lem4  28012  eupth2lem3lem6  28014  cycpmco2lem1  30770  cycpmco2lem4  30773  cycpmco2  30777  tgoldbachgt  31936  cvmliftmolem1  32530  neibastop3  33712  fdc  35022  pclvalN  37028  dvhb1dimN  38124  hdmaplkr  39051  diophren  39417  islmodfg  39676  fsovcnvlem  40366  ntrneiel  40438  radcnvrat  40653  supminfxr  41747  stoweidlem34  42326