Theorem elrab3 3672

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {crab 3415

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461

This theorem is referenced by:  unimax  4920  fnelfp  7167  fnelnfp  7169  fnse  8132  fin23lem30  10356  isf32lem5  10371  negn0  11666  ublbneg  12949  supminf  12951  sadval  16475  smuval  16500  dvdslcm  16617  dvdslcmf  16650  isprm2lem  16700  isacs1i  17669  isinito  18009  istermo  18010  subgacs  19144  nsgacs  19145  odngen  19558  sdrgacs  20761  lssacs  20924  mretopd  23030  txkgen  23590  xkoco1cn  23595  xkoco2cn  23596  xkoinjcn  23625  ordthmeolem  23739  shft2rab  25461  sca2rab  25465  lhop1lem  25970  ftalem5  27039  vmasum  27179  eqscut2  27770  elmade  27831  israg  28676  ebtwntg  28961  eupth2lem3lem3  30211  eupth2lem3lem4  30212  eupth2lem3lem6  30214  cycpmco2lem1  33137  cycpmco2lem4  33140  cycpmco2  33144  ssdifidllem  33471  1arithufdlem2  33560  tgoldbachgt  34695  cvmliftmolem1  35303  neibastop3  36380  fdc  37769  pclvalN  39909  dvhb1dimN  41005  hdmaplkr  41932  aks4d1p8  42100  sticksstones1  42159  fsuppssind  42616  diophren  42836  islmodfg  43093  fsovcnvlem  44037  ntrneiel  44105  radcnvrat  44338  supminfxr  45491  stoweidlem34  46063