Theorem cbvexv 1890

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

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

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cbvexvw  1892  eujust  2001  euind  2871  reuind  2889  r19.2m  3449  r19.3rm  3451  r19.9rmv  3454  raaanlem  3468  raaan  3469  cbvopab2v  4005  bm1.3ii  4049  mss  4148  zfun  4356  xpiindim  4676  relop  4689  dmmrnm  4758  dmxpm  4759  dmcoss  4808  xpm  4960  cnviinm  5080  fv3  5444  fo1stresm  6059  fo2ndresm  6060  tfr1onlemaccex  6245  tfrcllemaccex  6258  iinerm  6501  riinerm  6502  ixpiinm  6618  ac6sfi  6792  ctmlemr  6993  ctm  6994  ctssdclemr  6997  ctssdc  6998  fodjum  7018  acfun  7063  ccfunen  7079  ltexprlemdisj  7414  ltexprlemloc  7415  recexprlemdisj  7438  suplocsr  7617  axpre-suploc  7710  zfz1isolem1  10583  climmo  11067  summodc  11152  ctiunct  11953  neipsm  12323  suplociccex  12772  bdbm1.3ii  13089