Theorem elrab3 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432

This theorem is referenced by:  unimax  4888  fnelfp  7124  fnelnfp  7126  fnse  8077  fin23lem30  10258  isf32lem5  10273  negn0  11573  ublbneg  12877  supminf  12879  sadval  16419  smuval  16444  dvdslcm  16561  dvdslcmf  16594  isprm2lem  16644  isacs1i  17617  isinito  17957  istermo  17958  subgacs  19130  nsgacs  19131  odngen  19546  sdrgacs  20772  lssacs  20956  mretopd  23070  txkgen  23630  xkoco1cn  23635  xkoco2cn  23636  xkoinjcn  23665  ordthmeolem  23779  shft2rab  25488  sca2rab  25492  lhop1lem  25993  ftalem5  27057  vmasum  27196  eqcuts2  27795  elmade  27866  addonbday  28288  israg  28782  ebtwntg  29068  eupth2lem3lem3  30318  eupth2lem3lem4  30319  eupth2lem3lem6  30321  cycpmco2lem1  33205  cycpmco2lem4  33208  cycpmco2  33212  ssdifidllem  33534  1arithufdlem2  33623  tgoldbachgt  34826  cvmliftmolem1  35482  neibastop3  36563  fdc  38083  pclvalN  40353  dvhb1dimN  41449  hdmaplkr  42376  aks4d1p8  42543  sticksstones1  42602  fsuppssind  43043  diophren  43262  islmodfg  43518  fsovcnvlem  44461  ntrneiel  44529  radcnvrat  44762  supminfxr  45913  stoweidlem34  46483