Theorem elrab3 3660

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465

This theorem is referenced by:  unimax  4914  fnelfp  7174  fnelnfp  7176  fnse  8128  fin23lem30  10325  isf32lem5  10340  negn0  11642  ublbneg  12956  supminf  12958  sadval  16513  smuval  16538  dvdslcm  16655  dvdslcmf  16688  isprm2lem  16738  isacs1i  17712  isinito  18052  istermo  18053  subgacs  19226  nsgacs  19227  odngen  19646  sdrgacs  20881  lssacs  21065  ssdifidllem  21452  mretopd  23217  txkgen  23777  xkoco1cn  23782  xkoco2cn  23783  xkoinjcn  23812  ordthmeolem  23926  shft2rab  25635  sca2rab  25639  lhop1lem  26140  ftalem5  27206  vmasum  27345  eqcuts2  27944  elmade  28015  addonbday  28437  israg  28935  ebtwntg  29272  eupth2lem3lem3  30521  eupth2lem3lem4  30522  eupth2lem3lem6  30524  cycpmco2lem1  33386  cycpmco2lem4  33389  cycpmco2  33393  1arithufdlem2  33779  tgoldbachgt  34994  cvmliftmolem1  35671  nmulr0  36585  neibastop3  36761  fdc  38283  pclvalN  40553  dvhb1dimN  41649  hdmaplkr  42576  aks4d1p8  42743  sticksstones1  42802  fsuppssind  43216  diophren  43431  islmodfg  43687  fsovcnvlem  44630  ntrneiel  44698  radcnvrat  44915  supminfxr  46069  stoweidlem34  46639