Theorem cbvexv 1906

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

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

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  eujust  2016  euind  2913  reuind  2931  r19.2m  3495  r19.3rm  3497  r19.9rmv  3500  raaanlem  3514  raaan  3515  cbvopab2v  4059  bm1.3ii  4103  mss  4204  zfun  4412  xpiindim  4741  relop  4754  dmmrnm  4823  dmxpm  4824  dmcoss  4873  xpm  5025  cnviinm  5145  fv3  5509  fo1stresm  6129  fo2ndresm  6130  tfr1onlemaccex  6316  tfrcllemaccex  6329  iinerm  6573  riinerm  6574  ixpiinm  6690  ac6sfi  6864  ctmlemr  7073  ctm  7074  ctssdclemr  7077  ctssdc  7078  fodjum  7110  acfun  7163  ccfunen  7205  cc2lem  7207  cc2  7208  ltexprlemdisj  7547  ltexprlemloc  7548  recexprlemdisj  7571  suplocsr  7750  axpre-suploc  7843  zfz1isolem1  10753  climmo  11239  summodc  11324  nninfdcex  11886  zsupssdc  11887  ctiunct  12373  neipsm  12794  suplociccex  13243  bdbm1.3ii  13773