Theorem spvv 1990

Description: Specialization, using implicit substitution. Version of spv 2397 with a disjoint variable condition, which does not require ax-7 2010, ax-12 2185, ax-13 2376. (Contributed by NM, 30-Aug-1993.) (Revised by BJ, 31-May-2019.)

Hypothesis

Ref	Expression
spvv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spvv	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem spvv

Step	Hyp	Ref	Expression
1		spvv.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	biimpd 229	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimvw 1988	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  chvarvv  1991  ru0  2133  nfcr  2888  ruOLD  3727  nalsetOLD  5250  dfpo2  6260  isowe2  7305  tfisi  7810  findcard2  9099  marypha1lem  9346  elirrv  9512  setind  9668  karden  9819  kmlem4  10076  axgroth3  10754  ramcl  17000  cnsubrglem  21397  alexsubALTlem3  24014  i1fd  25648  r1omhfb  35256  setindregs  35274  r1omhfbregs  35281  dfon2lem6  35968  trer  36498  axtco1from2  36657  axtcond  36660  axuntco  36661  eleq2w2ALT  37354  modelaxreplem1  45405  elsetrecslem  50174