Theorem elrab3 3645

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  unimax  4904  fnelfp  7180  fnelnfp  7182  fnse  8150  fin23lem30  10420  isf32lem5  10435  negn0  11745  ublbneg  13060  supminf  13062  sadval  16626  smuval  16651  dvdslcm  16773  dvdslcmf  16806  isprm2lem  16856  isacs1i  17831  isinito  18171  istermo  18172  subgacs  19371  nsgacs  19372  odngen  19791  sdrgacs  21058  lssacs  21242  ssdifidllem  21640  mretopd  23410  txkgen  23971  xkoco1cn  23976  xkoco2cn  23977  xkoinjcn  24006  ordthmeolem  24120  shft2rab  25829  sca2rab  25833  lhop1lem  26333  ftalem5  27404  vmasum  27543  eqcuts2  28172  elmade  28243  addonbday  28665  israg  29172  ebtwntg  29560  eupth2lem3lem3  30831  eupth2lem3lem4  30832  eupth2lem3lem6  30834  cycpmco2lem1  33687  cycpmco2lem4  33690  cycpmco2  33694  1arithufdlem2  34077  tgoldbachgt  35292  cvmliftmolem1  36046  nmulr0  36944  neibastop3  37150  fdc  38680  pclvalN  40948  dvhb1dimN  42044  hdmaplkr  42971  aks4d1p8  43138  sticksstones1  43197  fsuppssind  43622  diophren  43820  islmodfg  44071  fsovcnvlem  45013  ntrneiel  45081  radcnvrat  45298  supminfxr  46474  stoweidlem34  47044