Theorem rspcdv 3562

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 228	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))
4	1, 3	rspcimdv 3560	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063

This theorem is referenced by:  rspcdv2  3565  rspcv  3566  ralxfrd  5344  ralxfrd2  5348  reuop  6216  suppofss1d  8065  suppofss2d  8066  zindd  12491  wrd2ind  14505  ismri2dad  17413  mreexd  17418  mreexexlemd  17420  catcocl  17461  catass  17462  moni  17515  subccocl  17627  funcco  17653  fullfo  17695  fthf1  17700  nati  17738  mndind  18533  idsrngd  20193  uspgr2wlkeq  28121  crctcshwlkn0lem4  28286  crctcshwlkn0lem5  28287  wwlknllvtx  28319  0enwwlksnge1  28337  wlkiswwlks2lem5  28346  clwlkclwwlklem2a  28470  clwlkclwwlklem2  28472  clwwisshclwws  28487  clwwlkinwwlk  28512  umgr2cwwk2dif  28536  wrdt2ind  31333  mgccole1  31376  mgccole2  31377  mgcmnt1  31378  mgcmntco  31380  dfmgc2lem  31381  rngurd  31590  fedgmullem2  31817  zart0  31935  zarcmplem  31937  esumcvg  32160  inelcarsg  32384  carsgclctunlem1  32390  orvcelel  32542  signsply0  32636  onint1  34699  qsalrel  40425  ismnushort  42147  ralbinrald  44873  fargshiftfva  45154  reupr  45233  evengpop3  45509  evengpoap3  45510  isomgrsym  45547  snlindsntorlem  46070