Theorem cbvexv 1916

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

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

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2026  euind  2922  reuind  2940  r19.2m  3507  r19.3rm  3509  r19.9rmv  3512  raaanlem  3526  raaan  3527  cbvopab2v  4075  bm1.3ii  4119  mss  4220  zfun  4428  xpiindim  4757  relop  4770  dmmrnm  4839  dmxpm  4840  dmcoss  4889  xpm  5042  cnviinm  5162  iotam  5200  fv3  5530  fo1stresm  6152  fo2ndresm  6153  tfr1onlemaccex  6339  tfrcllemaccex  6352  iinerm  6597  riinerm  6598  ixpiinm  6714  ac6sfi  6888  ctmlemr  7097  ctm  7098  ctssdclemr  7101  ctssdc  7102  fodjum  7134  acfun  7196  ccfunen  7238  cc2lem  7240  cc2  7241  ltexprlemdisj  7580  ltexprlemloc  7581  recexprlemdisj  7604  suplocsr  7783  axpre-suploc  7876  zfz1isolem1  10788  climmo  11274  summodc  11359  nninfdcex  11921  zsupssdc  11922  ctiunct  12408  ismnd  12695  dfgrp3me  12840  neipsm  13234  suplociccex  13683  bdbm1.3ii  14212