Theorem rspcdva 3316

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)

Hypotheses

Ref	Expression
rspcdva.1	⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
rspcdva.2	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
rspcdva.3	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
rspcdva	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rspcdva

Step	Hyp	Ref	Expression
1		rspcdva.2	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
2		rspcdva.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
3		rspcdva.1	. . . 4 ⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
4	3	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐶) → (𝜓 ↔ 𝜒))
5	2, 4	rspcdv 3312	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
6	1, 5	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 196   = 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:  grprinvlem  6872  grprinvd  6873  fin1ai  9115  seqshft2  12827  seqsplit  12834  prmreclem5  15624  gsumzaddlem  18321  ablfac1eu  18472  evlslem1  19515  mdetunilem1  20418  cmpcov  21192  cuspcvg  22105  tayl0  24116  lgamcvglem  24766  wlkonl1iedg  26561  wlkp1lem7  26576  wlkp1lem8  26577  crctcshwlkn0lem6  26707  eupth2eucrct  27077  inelpisys  30217  unelldsys  30221  ldgenpisyslem1  30226  fsum2dsub  30685  hgt750lemc  30725  hgt750lemd  30726  hgt749d  30727  hgt750lemf  30731  cvmlift2lem10  31294  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2  32502  climisp  39978  climrescn  39980  climxrrelem  39981  climxrre  39982  saldifcl  40539