Theorem rspcdv 3312

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  rspcdva  3316  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  suppofss1d  7332  suppofss2d  7333  zindd  11478  wrd2ind  13477  ismri2dad  16297  mreexd  16302  mreexexlemd  16304  catcocl  16346  catass  16347  moni  16396  subccocl  16505  funcco  16531  fullfo  16572  fthf1  16577  nati  16615  mrcmndind  17366  idsrngd  18862  flfcntr  21847  uspgr2wlkeq  26542  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  0enwwlksnge1  26749  wlkiswwlks2lem5  26759  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  clwwlkinwwlk  26905  clwwisshclwws  26928  umgr2cwwk2dif  26941  rngurd  29788  esumcvg  30148  inelcarsg  30373  carsgclctunlem1  30379  orvcelel  30531  signsply0  30628  onint1  32448  rspcdvinvd  38474  ralbinrald  41199  fargshiftfva  41379  evengpop3  41686  evengpoap3  41687  snlindsntorlem  42259