Theorem cbvexv 1943

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2057  euind  2961  reuind  2979  r19.2m  3548  r19.3rm  3550  r19.9rmv  3553  raaanlem  3566  raaan  3567  cbvopab2v  4125  bm1.3ii  4169  mss  4274  zfun  4485  xpiindim  4819  relop  4832  dmmrnm  4902  dmxpm  4903  dmcoss  4953  xpm  5109  cnviinm  5229  iotam  5268  fv3  5606  elfvm  5616  fo1stresm  6254  fo2ndresm  6255  tfr1onlemaccex  6441  tfrcllemaccex  6454  iinerm  6701  riinerm  6702  ixpiinm  6818  ac6sfi  7002  ctmlemr  7217  ctm  7218  ctssdclemr  7221  ctssdc  7222  fodjum  7255  finacn  7323  acfun  7326  ccfunen  7383  cc2lem  7385  cc2  7386  ltexprlemdisj  7726  ltexprlemloc  7727  recexprlemdisj  7750  suplocsr  7929  axpre-suploc  8022  nninfdcex  10387  zsupssdc  10388  zfz1isolem1  10992  climmo  11653  summodc  11738  nninfct  12406  ctiunct  12855  ismnd  13295  dfgrp3me  13476  issubg2m  13569  subrgintm  14049  islssm  14163  islidlm  14285  neipsm  14670  suplociccex  15141  bdbm1.3ii  15901