Theorem rspcdv 3613

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 3611	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061

This theorem is referenced by:  rspcdv2  3616  rspcv  3617  ralxfrd  5407  ralxfrd2  5411  reuop  6312  suppofss1d  8230  suppofss2d  8231  zindd  12721  wrd2ind  14762  ismri2dad  17681  mreexd  17686  mreexexlemd  17688  catcocl  17729  catass  17730  moni  17781  subccocl  17891  funcco  17917  fullfo  17960  fthf1  17965  nati  18004  mndind  18842  ringurd  20183  idsrngd  20858  mpomulcn  24892  fsumdvdsmul  27239  uspgr2wlkeq  29665  crctcshwlkn0lem4  29834  crctcshwlkn0lem5  29835  wwlknllvtx  29867  0enwwlksnge1  29885  wlkiswwlks2lem5  29894  clwlkclwwlklem2a  30018  clwlkclwwlklem2  30020  clwwisshclwws  30035  clwwlkinwwlk  30060  umgr2cwwk2dif  30084  wrdt2ind  32939  mgccole1  32981  mgccole2  32982  mgcmnt1  32983  mgcmntco  32985  dfmgc2lem  32986  chnind  33002  1arithufdlem3  33575  dfufd2  33579  fedgmullem2  33682  constrconj  33787  zart0  33879  zarcmplem  33881  esumcvg  34088  inelcarsg  34314  carsgclctunlem1  34320  orvcelel  34473  signsply0  34567  onint1  36451  qsalrel  42281  ismnushort  44325  ralbinrald  47139  fargshiftfva  47435  reupr  47514  evengpop3  47790  evengpoap3  47791  snlindsntorlem  48392