Theorem rspcdv 3570

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 3568	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  3573  rspcv  3574  ralxfrd  5355  ralxfrd2  5359  reuop  6259  suppofss1d  8156  suppofss2d  8157  zindd  12605  wrd2ind  14658  ismri2dad  17572  mreexd  17577  mreexexlemd  17579  catcocl  17620  catass  17621  moni  17672  subccocl  17781  funcco  17807  fullfo  17850  fthf1  17855  nati  17894  chnind  18556  mndind  18765  ringurd  20132  idsrngd  20801  mpomulcn  24826  fsumdvdsmul  27173  uspgr2wlkeq  29731  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wwlknllvtx  29931  0enwwlksnge1  29949  wlkiswwlks2lem5  29958  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwwisshclwws  30102  clwwlkinwwlk  30127  umgr2cwwk2dif  30151  wrdt2ind  33046  mgccole1  33083  mgccole2  33084  mgcmnt1  33085  mgcmntco  33087  dfmgc2lem  33088  1arithufdlem3  33639  dfufd2  33643  fedgmullem2  33808  constrconj  33923  zart0  34057  zarcmplem  34059  esumcvg  34264  inelcarsg  34489  carsgclctunlem1  34495  orvcelel  34648  signsply0  34729  onint1  36665  qsalrel  42611  ismnushort  44657  ralbinrald  47482  fargshiftfva  47803  reupr  47882  evengpop3  48158  evengpoap3  48159  snlindsntorlem  48830