Theorem cbvexv 1967

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

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

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2081  euind  2993  reuind  3011  r19.2m  3581  r19.3rm  3583  r19.9rmv  3586  raaanlem  3599  raaan  3600  cbvopab2v  4166  bm1.3ii  4210  mss  4318  zfun  4531  xpiindim  4867  relop  4880  reldmm  4950  dmmrnm  4951  dmxpm  4952  dmcoss  5002  xpm  5158  cnviinm  5278  iotam  5318  fv3  5662  elfvm  5672  fo1stresm  6324  fo2ndresm  6325  tfr1onlemaccex  6514  tfrcllemaccex  6527  iinerm  6776  riinerm  6777  ixpiinm  6893  ac6sfi  7087  ctmlemr  7307  ctm  7308  ctssdclemr  7311  ctssdc  7312  fodjum  7345  finacn  7419  acfun  7422  ccfunen  7483  cc2lem  7485  cc2  7486  ltexprlemdisj  7826  ltexprlemloc  7827  recexprlemdisj  7850  suplocsr  8029  axpre-suploc  8122  nninfdcex  10498  zsupssdc  10499  zfz1isolem1  11105  climmo  11860  summodc  11946  nninfct  12614  ctiunct  13063  ismnd  13504  dfgrp3me  13685  issubg2m  13778  subrgintm  14260  islssm  14374  islidlm  14496  neipsm  14881  suplociccex  15352  bdbm1.3ii  16507  gfsumval  16701