Theorem elrab3 3693

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482

This theorem is referenced by:  unimax  4944  fnelfp  7195  fnelnfp  7197  fnse  8158  fin23lem30  10382  isf32lem5  10397  negn0  11692  ublbneg  12975  supminf  12977  sadval  16493  smuval  16518  dvdslcm  16635  dvdslcmf  16668  isprm2lem  16718  isacs1i  17700  isinito  18041  istermo  18042  subgacs  19179  nsgacs  19180  odngen  19595  sdrgacs  20802  lssacs  20965  mretopd  23100  txkgen  23660  xkoco1cn  23665  xkoco2cn  23666  xkoinjcn  23695  ordthmeolem  23809  shft2rab  25543  sca2rab  25547  lhop1lem  26052  ftalem5  27120  vmasum  27260  eqscut2  27851  elmade  27906  israg  28705  ebtwntg  28997  eupth2lem3lem3  30249  eupth2lem3lem4  30250  eupth2lem3lem6  30252  cycpmco2lem1  33146  cycpmco2lem4  33149  cycpmco2  33153  ssdifidllem  33484  1arithufdlem2  33573  tgoldbachgt  34678  cvmliftmolem1  35286  neibastop3  36363  fdc  37752  pclvalN  39892  dvhb1dimN  40988  hdmaplkr  41915  aks4d1p8  42088  sticksstones1  42147  fsuppssind  42603  diophren  42824  islmodfg  43081  fsovcnvlem  44026  ntrneiel  44094  radcnvrat  44333  supminfxr  45475  stoweidlem34  46049