Theorem rspcdv 3553

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069

This theorem is referenced by:  rspcdv2  3556  rspcv  3557  ralxfrd  5331  ralxfrd2  5335  reuop  6196  suppofss1d  8020  suppofss2d  8021  zindd  12421  wrd2ind  14436  ismri2dad  17346  mreexd  17351  mreexexlemd  17353  catcocl  17394  catass  17395  moni  17448  subccocl  17560  funcco  17586  fullfo  17628  fthf1  17633  nati  17671  mndind  18466  idsrngd  20122  uspgr2wlkeq  28013  crctcshwlkn0lem4  28178  crctcshwlkn0lem5  28179  wwlknllvtx  28211  0enwwlksnge1  28229  wlkiswwlks2lem5  28238  clwlkclwwlklem2a  28362  clwlkclwwlklem2  28364  clwwisshclwws  28379  clwwlkinwwlk  28404  umgr2cwwk2dif  28428  wrdt2ind  31225  mgccole1  31268  mgccole2  31269  mgcmnt1  31270  mgcmntco  31272  dfmgc2lem  31273  rngurd  31482  fedgmullem2  31711  zart0  31829  zarcmplem  31831  esumcvg  32054  inelcarsg  32278  carsgclctunlem1  32284  orvcelel  32436  signsply0  32530  onint1  34638  qsalrel  40215  ismnushort  41919  ralbinrald  44614  fargshiftfva  44895  reupr  44974  evengpop3  45250  evengpoap3  45251  isomgrsym  45288  snlindsntorlem  45811