Theorem cbvexv 1966

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 1802	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  2080  euind  2992  reuind  3010  r19.2m  3580  r19.3rm  3582  r19.9rmv  3585  raaanlem  3598  raaan  3599  cbvopab2v  4167  bm1.3ii  4211  mss  4320  zfun  4533  xpiindim  4869  relop  4882  reldmm  4952  dmmrnm  4953  dmxpm  4954  dmcoss  5004  xpm  5160  cnviinm  5280  iotam  5320  fv3  5665  elfvm  5675  fo1stresm  6329  fo2ndresm  6330  tfr1onlemaccex  6519  tfrcllemaccex  6532  iinerm  6781  riinerm  6782  ixpiinm  6898  ac6sfi  7092  ctmlemr  7312  ctm  7313  ctssdclemr  7316  ctssdc  7317  fodjum  7350  finacn  7424  acfun  7427  ccfunen  7488  cc2lem  7490  cc2  7491  ltexprlemdisj  7831  ltexprlemloc  7832  recexprlemdisj  7855  suplocsr  8034  axpre-suploc  8127  nninfdcex  10503  zsupssdc  10504  zfz1isolem1  11110  climmo  11881  summodc  11967  nninfct  12635  ctiunct  13084  ismnd  13525  dfgrp3me  13706  issubg2m  13799  subrgintm  14281  islssm  14395  islidlm  14517  neipsm  14907  suplociccex  15378  bdbm1.3ii  16546  gfsumval  16748