Theorem cbvexv 1868

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  1975  euind  2838  reuind  2856  r19.2m  3413  r19.3rm  3415  r19.9rmv  3418  raaanlem  3432  raaan  3433  cbvopab2v  3963  bm1.3ii  4007  mss  4106  zfun  4314  xpiindim  4634  relop  4647  dmmrnm  4716  dmxpm  4717  dmcoss  4764  xpm  4916  cnviinm  5036  fv3  5396  fo1stresm  6011  fo2ndresm  6012  tfr1onlemaccex  6197  tfrcllemaccex  6210  iinerm  6453  riinerm  6454  ixpiinm  6570  ac6sfi  6743  ctmlemr  6943  ctm  6944  ctssdclemr  6947  ctssdc  6948  fodjum  6966  acfun  7008  ltexprlemdisj  7356  ltexprlemloc  7357  recexprlemdisj  7380  zfz1isolem1  10470  climmo  10953  summodc  11038  ctiunct  11790  neipsm  12160  bdbm1.3ii  12772