Theorem rspcdv 3533

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075

This theorem is referenced by:  rspcv  3536  ralxfrd  5277  ralxfrd2  5281  reuop  6122  suppofss1d  7878  suppofss2d  7879  zindd  12122  wrd2ind  14132  ismri2dad  16966  mreexd  16971  mreexexlemd  16973  catcocl  17014  catass  17015  moni  17065  subccocl  17174  funcco  17200  fullfo  17241  fthf1  17246  nati  17284  mndind  18058  idsrngd  19701  uspgr2wlkeq  27534  crctcshwlkn0lem4  27698  crctcshwlkn0lem5  27699  wwlknllvtx  27731  0enwwlksnge1  27749  wlkiswwlks2lem5  27758  clwlkclwwlklem2a  27882  clwlkclwwlklem2  27884  clwwisshclwws  27899  clwwlkinwwlk  27924  umgr2cwwk2dif  27948  wrdt2ind  30749  mgccole1  30794  mgccole2  30795  mgcmnt1  30796  mgcmntco  30798  dfmgc2lem  30799  rngurd  31008  fedgmullem2  31232  zart0  31350  zarcmplem  31352  esumcvg  31573  inelcarsg  31797  carsgclctunlem1  31803  orvcelel  31955  signsply0  32049  onint1  34187  qsalrel  39721  rspcdvinvd  41250  ralbinrald  44046  fargshiftfva  44328  reupr  44407  evengpop3  44683  evengpoap3  44684  isomgrsym  44721  snlindsntorlem  45244