Theorem rspcdv 3564

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1525   ∈ wcel 2083  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-ral 3112  df-v 3442

This theorem is referenced by:  ralxfrd  5207  ralxfrd2  5211  reuop  6026  suppofss1d  7726  suppofss2d  7727  zindd  11937  wrd2ind  13925  ismri2dad  16741  mreexd  16746  mreexexlemd  16748  catcocl  16789  catass  16790  moni  16839  subccocl  16948  funcco  16974  fullfo  17015  fthf1  17020  nati  17058  mndind  17809  idsrngd  19327  uspgr2wlkeq  27114  crctcshwlkn0lem4  27277  crctcshwlkn0lem5  27278  wwlknllvtx  27310  0enwwlksnge1  27328  wlkiswwlks2lem5  27337  clwlkclwwlklem2a  27462  clwlkclwwlklem2  27464  clwwisshclwws  27479  clwwlkinwwlk  27504  umgr2cwwk2dif  27529  wrdt2ind  30302  rngurd  30507  fedgmullem2  30626  esumcvg  30958  inelcarsg  31182  carsgclctunlem1  31188  orvcelel  31340  signsply0  31434  onint1  33408  qsalrel  38676  rspcdvinvd  40031  ralbinrald  42859  fargshiftfva  43107  reupr  43188  evengpop3  43467  evengpoap3  43468  isomgrsym  43505  snlindsntorlem  44027