Theorem cbvexv 1965

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2079  euind  2991  reuind  3009  r19.2m  3579  r19.3rm  3581  r19.9rmv  3584  raaanlem  3597  raaan  3598  cbvopab2v  4164  bm1.3ii  4208  mss  4316  zfun  4529  xpiindim  4865  relop  4878  reldmm  4948  dmmrnm  4949  dmxpm  4950  dmcoss  5000  xpm  5156  cnviinm  5276  iotam  5316  fv3  5658  elfvm  5668  fo1stresm  6319  fo2ndresm  6320  tfr1onlemaccex  6509  tfrcllemaccex  6522  iinerm  6771  riinerm  6772  ixpiinm  6888  ac6sfi  7082  ctmlemr  7301  ctm  7302  ctssdclemr  7305  ctssdc  7306  fodjum  7339  finacn  7412  acfun  7415  ccfunen  7476  cc2lem  7478  cc2  7479  ltexprlemdisj  7819  ltexprlemloc  7820  recexprlemdisj  7843  suplocsr  8022  axpre-suploc  8115  nninfdcex  10490  zsupssdc  10491  zfz1isolem1  11097  climmo  11852  summodc  11937  nninfct  12605  ctiunct  13054  ismnd  13495  dfgrp3me  13676  issubg2m  13769  subrgintm  14250  islssm  14364  islidlm  14486  neipsm  14871  suplociccex  15342  bdbm1.3ii  16436  gfsumval  16630