Theorem elrab3 3709

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490

This theorem is referenced by:  unimax  4968  fnelfp  7209  fnelnfp  7211  fnse  8174  fin23lem30  10411  isf32lem5  10426  negn0  11719  ublbneg  12998  supminf  13000  sadval  16502  smuval  16527  dvdslcm  16645  dvdslcmf  16678  isprm2lem  16728  isacs1i  17715  isinito  18063  istermo  18064  subgacs  19201  nsgacs  19202  odngen  19619  sdrgacs  20824  lssacs  20988  mretopd  23121  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkoinjcn  23716  ordthmeolem  23830  shft2rab  25562  sca2rab  25566  lhop1lem  26072  ftalem5  27138  vmasum  27278  eqscut2  27869  elmade  27924  israg  28723  ebtwntg  29015  eupth2lem3lem3  30262  eupth2lem3lem4  30263  eupth2lem3lem6  30265  cycpmco2lem1  33119  cycpmco2lem4  33122  cycpmco2  33126  ssdifidllem  33449  1arithufdlem2  33538  tgoldbachgt  34640  cvmliftmolem1  35249  neibastop3  36328  fdc  37705  pclvalN  39847  dvhb1dimN  40943  hdmaplkr  41870  aks4d1p8  42044  sticksstones1  42103  fsuppssind  42548  diophren  42769  islmodfg  43026  fsovcnvlem  43975  ntrneiel  44043  radcnvrat  44283  supminfxr  45379  stoweidlem34  45955