Theorem rspcdv 3557

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspcdv2  3560  rspcv  3561  ralxfrd  5345  ralxfrd2  5349  reuop  6251  suppofss1d  8147  suppofss2d  8148  zindd  12621  wrd2ind  14676  ismri2dad  17594  mreexd  17599  mreexexlemd  17601  catcocl  17642  catass  17643  moni  17694  subccocl  17803  funcco  17829  fullfo  17872  fthf1  17877  nati  17916  chnind  18578  mndind  18787  ringurd  20157  idsrngd  20824  mpomulcn  24844  fsumdvdsmul  27172  uspgr2wlkeq  29729  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  wwlknllvtx  29929  0enwwlksnge1  29947  wlkiswwlks2lem5  29956  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwwisshclwws  30100  clwwlkinwwlk  30125  umgr2cwwk2dif  30149  wrdt2ind  33028  mgccole1  33065  mgccole2  33066  mgcmnt1  33067  mgcmntco  33069  dfmgc2lem  33070  1arithufdlem3  33621  dfufd2  33625  fedgmullem2  33790  constrconj  33905  zart0  34039  zarcmplem  34041  esumcvg  34246  inelcarsg  34471  carsgclctunlem1  34477  orvcelel  34630  signsply0  34711  onint1  36647  qsalrel  42694  ismnushort  44746  ralbinrald  47582  fargshiftfva  47915  reupr  47994  evengpop3  48286  evengpoap3  48287  snlindsntorlem  48958