Theorem elrab3 3653

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {crab 3418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459

This theorem is used by:  unimax  4912  fnelfp  7179  fnelnfp  7181  fnse  8135  fin23lem30  10341  isf32lem5  10356  negn0  11658  ublbneg  12973  supminf  12975  sadval  16536  smuval  16561  dvdslcm  16678  dvdslcmf  16711  isprm2lem  16761  isacs1i  17735  isinito  18075  istermo  18076  subgacs  19271  nsgacs  19272  odngen  19691  sdrgacs  20954  lssacs  21138  ssdifidllem  21534  mretopd  23299  txkgen  23860  xkoco1cn  23865  xkoco2cn  23866  xkoinjcn  23895  ordthmeolem  24009  shft2rab  25718  sca2rab  25722  lhop1lem  26223  ftalem5  27292  vmasum  27431  eqcuts2  28030  elmade  28101  addonbday  28523  israg  29028  ebtwntg  29387  eupth2lem3lem3  30652  eupth2lem3lem4  30653  eupth2lem3lem6  30655  cycpmco2lem1  33510  cycpmco2lem4  33513  cycpmco2  33517  1arithufdlem2  33899  tgoldbachgt  35115  cvmliftmolem1  35810  nmulr0  36724  neibastop3  36930  fdc  38454  pclvalN  40722  dvhb1dimN  41818  hdmaplkr  42745  aks4d1p8  42912  sticksstones1  42971  fsuppssind  43383  diophren  43598  islmodfg  43854  fsovcnvlem  44797  ntrneiel  44865  radcnvrat  45082  supminfxr  46236  stoweidlem34  46806