Theorem cbvexv 1970

Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
cbvexv	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥

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

Proof of Theorem cbvexv

Step	Hyp	Ref	Expression
1		ax-17 1575	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
2		ax-17 1575	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		cbvalv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvexh 1804	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2084  euind  3006  reuind  3024  r19.2m  3598  r19.3rm  3600  r19.9rmv  3603  raaanlem  3616  raaan  3617  cbvopab2v  4189  bm1.3ii  4233  mss  4344  zfun  4557  xpiindim  4894  relop  4907  reldmm  4977  dmmrnm  4978  dmxpm  4979  dmcoss  5029  xpm  5186  cnviinm  5306  iotam  5346  fv3  5695  elfvm  5705  fo1stresm  6357  fo2ndresm  6358  tfr1onlemaccex  6581  tfrcllemaccex  6594  iinerm  6843  riinerm  6844  ixpiinm  6961  ac6sfi  7157  ctmlemr  7401  ctm  7402  ctssdclemr  7405  ctssdc  7406  fodjum  7439  finacn  7513  acfun  7516  ccfunen  7583  cc2lem  7585  cc2  7586  ltexprlemdisj  7926  ltexprlemloc  7927  recexprlemdisj  7950  suplocsr  8129  axpre-suploc  8222  nninfdcex  10604  zsupssdc  10605  zfz1isolem1  11220  climmo  11991  summodc  12077  nninfct  12745  ctiunct  13212  ismnd  13653  dfgrp3me  13834  issubg2m  13927  subrgintm  14411  islssm  14554  islidlm  14676  neipsm  15068  suplociccex  15539  bdbm1.3ii  16710  gfsumval  16911