Theorem cbvexv 1905

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 1513	. 2 ⊢ (𝜑 → ∀𝑦𝜑)
2		ax-17 1513	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
3		cbvalv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvexh 1742	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  2015  euind  2908  reuind  2926  r19.2m  3490  r19.3rm  3492  r19.9rmv  3495  raaanlem  3509  raaan  3510  cbvopab2v  4053  bm1.3ii  4097  mss  4198  zfun  4406  xpiindim  4735  relop  4748  dmmrnm  4817  dmxpm  4818  dmcoss  4867  xpm  5019  cnviinm  5139  fv3  5503  fo1stresm  6121  fo2ndresm  6122  tfr1onlemaccex  6307  tfrcllemaccex  6320  iinerm  6564  riinerm  6565  ixpiinm  6681  ac6sfi  6855  ctmlemr  7064  ctm  7065  ctssdclemr  7068  ctssdc  7069  fodjum  7101  acfun  7154  ccfunen  7196  cc2lem  7198  cc2  7199  ltexprlemdisj  7538  ltexprlemloc  7539  recexprlemdisj  7562  suplocsr  7741  axpre-suploc  7834  zfz1isolem1  10739  climmo  11225  summodc  11310  nninfdcex  11871  zsupssdc  11872  ctiunct  12310  neipsm  12695  suplociccex  13144  bdbm1.3ii  13608