Theorem elrab3 3646

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453

This theorem is used by:  unimax  4905  fnelfp  7178  fnelnfp  7180  fnse  8143  fin23lem30  10413  isf32lem5  10428  negn0  11738  ublbneg  13053  supminf  13055  sadval  16619  smuval  16644  dvdslcm  16766  dvdslcmf  16799  isprm2lem  16849  isacs1i  17824  isinito  18164  istermo  18165  subgacs  19364  nsgacs  19365  odngen  19784  sdrgacs  21051  lssacs  21235  ssdifidllem  21633  mretopd  23403  txkgen  23964  xkoco1cn  23969  xkoco2cn  23970  xkoinjcn  23999  ordthmeolem  24113  shft2rab  25822  sca2rab  25826  lhop1lem  26326  ftalem5  27397  vmasum  27536  eqcuts2  28165  elmade  28236  addonbday  28658  israg  29165  ebtwntg  29553  eupth2lem3lem3  30824  eupth2lem3lem4  30825  eupth2lem3lem6  30827  cycpmco2lem1  33680  cycpmco2lem4  33683  cycpmco2  33687  1arithufdlem2  34070  tgoldbachgt  35285  cvmliftmolem1  36025  nmulr0  36924  neibastop3  37130  fdc  38659  pclvalN  40927  dvhb1dimN  42023  hdmaplkr  42950  aks4d1p8  43117  sticksstones1  43176  fsuppssind  43601  diophren  43799  islmodfg  44055  fsovcnvlem  44998  ntrneiel  45066  radcnvrat  45283  supminfxr  46443  stoweidlem34  47013