Theorem chvarfv 2240

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2402 with a disjoint variable condition, which does not require ax-13 2379. (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 2239	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1799	1 ⊢ 𝜓

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

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786

This theorem is referenced by:  csbhypf  3856  axrep2  5157  axrep3  5158  opelopabsb  5382  isso2i  5472  wfisg  6151  tfindes  7557  findes  7593  dfoprab4f  7736  dom2lem  8532  pwfseqlem4a  10072  pwfseqlem4  10073  uzind4s  12296  seqof2  13424  fsumsplitf  15090  fproddivf  15333  fprodsplitf  15334  gsumcom2  19088  mdetralt2  21214  mdetunilem2  21218  ptcldmpt  22219  elmptrab  22432  isfildlem  22462  dvmptfsum  24578  dvfsumlem2  24630  lgamgulmlem2  25615  fmptcof2  30420  aciunf1lem  30425  fsumiunle  30571  esum2dlem  31461  fiunelros  31543  measiun  31587  bnj849  32307  bnj1014  32343  bnj1384  32414  bnj1489  32438  bnj1497  32442  setinds  33136  frpoinsg  33194  frinsg  33200  finxpreclem6  34813  ptrest  35056  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  fdc1  35184  fsumshftd  36248  fphpd  39757  monotuz  39882  monotoddzz  39884  oddcomabszz  39885  setindtrs  39966  flcidc  40118  binomcxplemnotnn0  41060  fiiuncl  41699  disjf1  41809  disjinfi  41820  supxrleubrnmptf  42090  monoordxr  42122  monoord2xr  42124  fsumclf  42211  fsummulc1f  42212  fsumnncl  42213  fsumf1of  42216  fsumiunss  42217  fsumreclf  42218  fsumlessf  42219  fsumsermpt  42221  fmul01  42222  fmuldfeq  42225  fmul01lt1lem1  42226  fmul01lt1lem2  42227  fprodexp  42236  fprodabs2  42237  climmulf  42246  climexp  42247  climsuse  42250  climrecf  42251  climinff  42253  climaddf  42257  mullimc  42258  neglimc  42289  addlimc  42290  0ellimcdiv  42291  climsubmpt  42302  climreclf  42306  climeldmeqmpt  42310  climfveqmpt  42313  fnlimfvre  42316  climfveqf  42322  climfveqmpt3  42324  climeldmeqf  42325  climeqf  42330  climeldmeqmpt3  42331  climinf2  42349  climinf2mpt  42356  climinfmpt  42357  limsupequz  42365  limsupequzmptf  42373  fprodcncf  42542  dvmptmulf  42579  dvnmptdivc  42580  dvnmul  42585  dvmptfprod  42587  stoweidlem3  42645  stoweidlem34  42676  stoweidlem42  42684  stoweidlem48  42690  fourierdlem112  42860  sge0lempt  43049  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0ltfirpmpt2  43065  sge0isummpt2  43071  sge0xaddlem2  43073  sge0xadd  43074  meadjiun  43105  voliunsge0lem  43111  meaiunincf  43122  meaiuninc3  43124  meaiininc  43126  hoimbl2  43304  vonhoire  43311  vonn0ioo2  43329  vonn0icc2  43331  salpreimagtlt  43364