Theorem elrab3 3506

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2140  {crab 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343

This theorem is referenced by:  unimax  4626  fnelfp  6607  fnelnfp  6609  fnse  7464  fin23lem30  9377  isf32lem5  9392  negn0  10672  ublbneg  11987  supminf  11989  sadval  15401  smuval  15426  dvdslcm  15534  dvdslcmf  15567  isprm2lem  15617  isacs1i  16540  isinito  16872  istermo  16873  subgacs  17851  nsgacs  17852  odngen  18213  lssacs  19190  mretopd  21119  txkgen  21678  xkoco1cn  21683  xkoco2cn  21684  xkoinjcn  21713  ordthmeolem  21827  shft2rab  23497  sca2rab  23501  lhop1lem  23996  ftalem5  25024  vmasum  25162  israg  25813  ebtwntg  26083  eupth2lem3lem3  27404  eupth2lem3lem4  27405  eupth2lem3lem6  27407  tgoldbachgt  31072  cvmliftmolem1  31592  neibastop3  32685  fdc  33873  pclvalN  35698  dvhb1dimN  36795  hdmaplkr  37726  diophren  37898  islmodfg  38160  sdrgacs  38292  fsovcnvlem  38828  ntrneiel  38900  radcnvrat  39034  supminfxr  40211  stoweidlem34  40773