Theorem chvarfv 2242

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2396 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
chvarfv.nf	⊢ Ⅎ𝑥𝜓
chvarfv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvarfv.2	⊢ 𝜑

Assertion

Ref	Expression
chvarfv	⊢ 𝜓

Distinct variable group:   𝑥,𝑦

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

Proof of Theorem chvarfv

Step	Hyp	Ref	Expression
1		chvarfv.nf	. . 3 ⊢ Ⅎ𝑥𝜓
2		chvarfv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpd 232	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2241	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1804	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-ex 1787  df-nf 1791

This theorem is referenced by:  csbhypf  3819  axrep2  5158  axrep3  5159  isso2i  5478  wfisg  6165  tfindes  7599  findes  7636  dfoprab4f  7782  dom2lem  8598  pwfseqlem4a  10164  pwfseqlem4  10165  uzind4s  12393  seqof2  13523  fsumsplitf  15194  fproddivf  15436  fprodsplitf  15437  gsumcom2  19217  mdetralt2  21363  mdetunilem2  21367  ptcldmpt  22368  elmptrab  22581  isfildlem  22611  dvmptfsum  24730  dvfsumlem2  24782  lgamgulmlem2  25770  fmptcof2  30572  aciunf1lem  30577  fsumiunle  30721  esum2dlem  31633  fiunelros  31715  measiun  31759  bnj849  32479  bnj1014  32515  bnj1384  32586  bnj1489  32610  bnj1497  32614  setinds  33331  frpoinsg  33389  frinsg  33398  finxpreclem6  35213  ptrest  35422  poimirlem24  35447  poimirlem25  35448  poimirlem26  35449  fdc1  35550  fsumshftd  36612  fphpd  40233  monotuz  40358  monotoddzz  40360  oddcomabszz  40361  setindtrs  40442  flcidc  40594  binomcxplemnotnn0  41535  fiiuncl  42174  disjf1  42281  disjinfi  42292  supxrleubrnmptf  42554  monoordxr  42586  monoord2xr  42588  fsumclf  42675  fsummulc1f  42676  fsumnncl  42677  fsumf1of  42680  fsumiunss  42681  fsumreclf  42682  fsumlessf  42683  fsumsermpt  42685  fmul01  42686  fmuldfeq  42689  fmul01lt1lem1  42690  fmul01lt1lem2  42691  fprodexp  42700  fprodabs2  42701  climmulf  42710  climexp  42711  climsuse  42714  climrecf  42715  climinff  42717  climaddf  42721  mullimc  42722  neglimc  42753  addlimc  42754  0ellimcdiv  42755  climsubmpt  42766  climreclf  42770  climeldmeqmpt  42774  climfveqmpt  42777  fnlimfvre  42780  climfveqf  42786  climfveqmpt3  42788  climeldmeqf  42789  climeqf  42794  climeldmeqmpt3  42795  climinf2  42813  climinf2mpt  42820  climinfmpt  42821  limsupequz  42829  limsupequzmptf  42837  fprodcncf  43006  dvmptmulf  43043  dvnmptdivc  43044  dvnmul  43049  dvmptfprod  43051  stoweidlem3  43109  stoweidlem34  43140  stoweidlem42  43148  stoweidlem48  43154  fourierdlem112  43324  sge0lempt  43513  sge0iunmptlemfi  43516  sge0iunmptlemre  43518  sge0iunmpt  43521  sge0ltfirpmpt2  43529  sge0isummpt2  43535  sge0xaddlem2  43537  sge0xadd  43538  meadjiun  43569  voliunsge0lem  43575  meaiunincf  43586  meaiuninc3  43588  meaiininc  43590  hoimbl2  43768  vonhoire  43775  vonn0ioo2  43793  vonn0icc2  43795  salpreimagtlt  43828