Theorem elrab3 3651

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457

This theorem is referenced by:  unimax  4910  fnelfp  7173  fnelnfp  7175  fnse  8125  fin23lem30  10321  isf32lem5  10336  negn0  11638  ublbneg  12952  supminf  12954  sadval  16509  smuval  16534  dvdslcm  16651  dvdslcmf  16684  isprm2lem  16734  isacs1i  17708  isinito  18048  istermo  18049  subgacs  19222  nsgacs  19223  odngen  19642  sdrgacs  20904  lssacs  21088  ssdifidllem  21484  mretopd  23249  txkgen  23809  xkoco1cn  23814  xkoco2cn  23815  xkoinjcn  23844  ordthmeolem  23958  shft2rab  25667  sca2rab  25671  lhop1lem  26172  ftalem5  27241  vmasum  27380  eqcuts2  27979  elmade  28050  addonbday  28472  israg  28977  ebtwntg  29332  eupth2lem3lem3  30581  eupth2lem3lem4  30582  eupth2lem3lem6  30584  cycpmco2lem1  33446  cycpmco2lem4  33449  cycpmco2  33453  1arithufdlem2  33835  tgoldbachgt  35050  cvmliftmolem1  35773  nmulr0  36687  neibastop3  36873  fdc  38396  pclvalN  40664  dvhb1dimN  41760  hdmaplkr  42687  aks4d1p8  42854  sticksstones1  42913  fsuppssind  43325  diophren  43540  islmodfg  43796  fsovcnvlem  44739  ntrneiel  44807  radcnvrat  45024  supminfxr  46178  stoweidlem34  46748