Theorem elrab3 3696

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480

This theorem is referenced by:  unimax  4949  fnelfp  7195  fnelnfp  7197  fnse  8157  fin23lem30  10380  isf32lem5  10395  negn0  11690  ublbneg  12973  supminf  12975  sadval  16490  smuval  16515  dvdslcm  16632  dvdslcmf  16665  isprm2lem  16715  isacs1i  17702  isinito  18050  istermo  18051  subgacs  19192  nsgacs  19193  odngen  19610  sdrgacs  20819  lssacs  20983  mretopd  23116  txkgen  23676  xkoco1cn  23681  xkoco2cn  23682  xkoinjcn  23711  ordthmeolem  23825  shft2rab  25557  sca2rab  25561  lhop1lem  26067  ftalem5  27135  vmasum  27275  eqscut2  27866  elmade  27921  israg  28720  ebtwntg  29012  eupth2lem3lem3  30259  eupth2lem3lem4  30260  eupth2lem3lem6  30262  cycpmco2lem1  33129  cycpmco2lem4  33132  cycpmco2  33136  ssdifidllem  33464  1arithufdlem2  33553  tgoldbachgt  34657  cvmliftmolem1  35266  neibastop3  36345  fdc  37732  pclvalN  39873  dvhb1dimN  40969  hdmaplkr  41896  aks4d1p8  42069  sticksstones1  42128  fsuppssind  42580  diophren  42801  islmodfg  43058  fsovcnvlem  44003  ntrneiel  44071  radcnvrat  44310  supminfxr  45414  stoweidlem34  45990