Theorem chvarfv 2229

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2390 with a disjoint variable condition, which does not require ax-13 2367. (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 228	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2228	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1792	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-12 2167

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779

This theorem is referenced by:  csbhypf  3921  axrep2  5288  axrep3  5289  isso2i  5625  frpoinsg  6349  wfisgOLD  6360  tfindes  7867  findes  7908  dfoprab4f  8060  dom2lem  9013  frinsg  9775  pwfseqlem4a  10685  pwfseqlem4  10686  uzind4s  12923  seqof2  14058  fsumclf  15717  fsumsplitf  15721  fproddivf  15964  fprodsplitf  15965  gsumcom2  19930  mdetralt2  22524  mdetunilem2  22528  ptcldmpt  23531  elmptrab  23744  isfildlem  23774  dvmptfsum  25920  dvfsumlem2  25974  dvfsumlem2OLD  25975  lgamgulmlem2  26975  fmptcof2  32456  aciunf1lem  32461  fsumiunle  32605  esum2dlem  33711  fiunelros  33793  measiun  33837  bnj849  34556  bnj1014  34592  bnj1384  34663  bnj1489  34687  bnj1497  34691  setinds  35374  finxpreclem6  36875  ptrest  37092  poimirlem24  37117  poimirlem25  37118  poimirlem26  37119  fdc1  37219  fsumshftd  38424  fphpd  42236  monotuz  42362  monotoddzz  42364  oddcomabszz  42365  setindtrs  42446  flcidc  42598  binomcxplemnotnn0  43793  fiiuncl  44429  disjf1  44556  disjinfi  44565  supxrleubrnmptf  44833  monoordxr  44865  monoord2xr  44867  fsummulc1f  44959  fsumnncl  44960  fsumf1of  44962  fsumiunss  44963  fsumreclf  44964  fsumlessf  44965  fsumsermpt  44967  fmul01  44968  fmuldfeq  44971  fmul01lt1lem1  44972  fmul01lt1lem2  44973  fprodexp  44982  fprodabs2  44983  climmulf  44992  climexp  44993  climsuse  44996  climrecf  44997  climinff  44999  climaddf  45003  mullimc  45004  neglimc  45035  addlimc  45036  0ellimcdiv  45037  climsubmpt  45048  climreclf  45052  climeldmeqmpt  45056  climfveqmpt  45059  fnlimfvre  45062  climfveqf  45068  climfveqmpt3  45070  climeldmeqf  45071  climeqf  45076  climeldmeqmpt3  45077  climinf2  45095  climinf2mpt  45102  climinfmpt  45103  limsupequz  45111  limsupequzmptf  45119  fprodcncf  45288  dvmptmulf  45325  dvnmptdivc  45326  dvnmul  45331  dvmptfprod  45333  stoweidlem3  45391  stoweidlem34  45422  stoweidlem42  45430  stoweidlem48  45436  fourierdlem112  45606  sge0lempt  45798  sge0iunmptlemfi  45801  sge0iunmptlemre  45803  sge0iunmpt  45806  sge0ltfirpmpt2  45814  sge0isummpt2  45820  sge0xaddlem2  45822  sge0xadd  45823  meadjiun  45854  voliunsge0lem  45860  meaiunincf  45871  meaiuninc3  45873  meaiininc  45875  hoimbl2  46053  vonhoire  46060  vonn0ioo2  46078  vonn0icc2  46080  salpreimagtlt  46118

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »