Theorem cbvexv 1968

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

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

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2082  euind  3003  reuind  3021  r19.2m  3595  r19.3rm  3597  r19.9rmv  3600  raaanlem  3613  raaan  3614  cbvopab2v  4186  bm1.3ii  4230  mss  4341  zfun  4554  xpiindim  4891  relop  4904  reldmm  4974  dmmrnm  4975  dmxpm  4976  dmcoss  5026  xpm  5183  cnviinm  5303  iotam  5343  fv3  5692  elfvm  5702  fo1stresm  6354  fo2ndresm  6355  tfr1onlemaccex  6578  tfrcllemaccex  6591  iinerm  6840  riinerm  6841  ixpiinm  6958  ac6sfi  7154  ctmlemr  7398  ctm  7399  ctssdclemr  7402  ctssdc  7403  fodjum  7436  finacn  7510  acfun  7513  ccfunen  7574  cc2lem  7576  cc2  7577  ltexprlemdisj  7917  ltexprlemloc  7918  recexprlemdisj  7941  suplocsr  8120  axpre-suploc  8213  nninfdcex  10593  zsupssdc  10594  zfz1isolem1  11205  climmo  11976  summodc  12062  nninfct  12730  ctiunct  13180  ismnd  13621  dfgrp3me  13802  issubg2m  13895  subrgintm  14377  islssm  14492  islidlm  14614  neipsm  15006  suplociccex  15477  bdbm1.3ii  16648  gfsumval  16848