Theorem rspcdv 3556

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)

Hypotheses

Ref	Expression
rspcdv.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
rspcdv.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rspcdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝜒,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcdv

Step	Hyp	Ref	Expression
1		rspcdv.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		rspcdv.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
3	2	biimpd 229	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))
4	1, 3	rspcimdv 3554	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspcdv2  3559  rspcv  3560  ralxfrd  5350  ralxfrd2  5354  reuop  6257  suppofss1d  8154  suppofss2d  8155  zindd  12630  wrd2ind  14685  ismri2dad  17603  mreexd  17608  mreexexlemd  17610  catcocl  17651  catass  17652  moni  17703  subccocl  17812  funcco  17838  fullfo  17881  fthf1  17886  nati  17925  chnind  18587  mndind  18796  ringurd  20166  idsrngd  20833  mpomulcn  24834  fsumdvdsmul  27158  uspgr2wlkeq  29714  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wwlknllvtx  29914  0enwwlksnge1  29932  wlkiswwlks2lem5  29941  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwwisshclwws  30085  clwwlkinwwlk  30110  umgr2cwwk2dif  30134  wrdt2ind  33013  mgccole1  33050  mgccole2  33051  mgcmnt1  33052  mgcmntco  33054  dfmgc2lem  33055  1arithufdlem3  33606  dfufd2  33610  fedgmullem2  33774  constrconj  33889  zart0  34023  zarcmplem  34025  esumcvg  34230  inelcarsg  34455  carsgclctunlem1  34461  orvcelel  34614  signsply0  34695  onint1  36631  qsalrel  42680  ismnushort  44728  ralbinrald  47570  fargshiftfva  47903  reupr  47982  evengpop3  48274  evengpoap3  48275  snlindsntorlem  48946