Theorem elrab3 3685

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {crab 3430

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474

This theorem is referenced by:  unimax  4949  fnelfp  7176  fnelnfp  7178  fnse  8123  fin23lem30  10341  isf32lem5  10356  negn0  11649  ublbneg  12923  supminf  12925  sadval  16403  smuval  16428  dvdslcm  16541  dvdslcmf  16574  isprm2lem  16624  isacs1i  17607  isinito  17952  istermo  17953  subgacs  19079  nsgacs  19080  odngen  19488  sdrgacs  20562  lssacs  20724  mretopd  22818  txkgen  23378  xkoco1cn  23383  xkoco2cn  23384  xkoinjcn  23413  ordthmeolem  23527  shft2rab  25259  sca2rab  25263  lhop1lem  25764  ftalem5  26815  vmasum  26953  eqscut2  27542  elmade  27597  israg  28213  ebtwntg  28505  eupth2lem3lem3  29748  eupth2lem3lem4  29749  eupth2lem3lem6  29751  cycpmco2lem1  32553  cycpmco2lem4  32556  cycpmco2  32560  tgoldbachgt  33971  cvmliftmolem1  34568  neibastop3  35552  fdc  36918  pclvalN  39066  dvhb1dimN  40162  hdmaplkr  41089  aks4d1p8  41260  sticksstones1  41270  fsuppssind  41469  diophren  41855  islmodfg  42115  fsovcnvlem  43068  ntrneiel  43136  radcnvrat  43377  supminfxr  44474  stoweidlem34  45050