Theorem cbvexv 1974

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

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

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2088  euind  3013  reuind  3031  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  cbvopab2v  4206  bm1.3ii  4252  mss  4364  zfun  4577  xpiindim  4915  relop  4928  reldmm  4998  dmmrnm  4999  dmxpm  5000  dmcoss  5050  xpm  5207  cnviinm  5327  iotam  5367  fv3  5716  elfvm  5726  mptmex  5939  fo1stresm  6389  fo2ndresm  6390  tfr1onlemaccex  6613  tfrcllemaccex  6626  iinerm  6875  riinerm  6876  ixpiinm  7000  ac6sfi  7196  ctmlemr  7442  ctm  7443  ctssdclemr  7446  ctssdc  7447  fodjum  7480  finacn  7554  acfun  7557  ccfunen  7624  cc2lem  7626  cc2  7627  ltexprlemdisj  7967  ltexprlemloc  7968  recexprlemdisj  7991  suplocsr  8170  axpre-suploc  8263  nninfdcex  10655  zsupssdc  10656  zfz1isolem1  11275  climmo  12047  summodc  12133  nninfct  12801  ctiunct  13314  ismnd  13715  dfgrp3me  13888  issubg2m  13975  gsumvalfi  14135  subrgintm  14534  islssm  14677  islidlm  14799  neipsm  15238  suplociccex  15709  bdbm1.3ii  16900