Theorem cbvexv 1965

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2079  euind  2990  reuind  3008  r19.2m  3578  r19.3rm  3580  r19.9rmv  3583  raaanlem  3596  raaan  3597  cbvopab2v  4161  bm1.3ii  4205  mss  4313  zfun  4526  xpiindim  4862  relop  4875  reldmm  4945  dmmrnm  4946  dmxpm  4947  dmcoss  4997  xpm  5153  cnviinm  5273  iotam  5313  fv3  5655  elfvm  5665  fo1stresm  6316  fo2ndresm  6317  tfr1onlemaccex  6505  tfrcllemaccex  6518  iinerm  6767  riinerm  6768  ixpiinm  6884  ac6sfi  7073  ctmlemr  7291  ctm  7292  ctssdclemr  7295  ctssdc  7296  fodjum  7329  finacn  7402  acfun  7405  ccfunen  7466  cc2lem  7468  cc2  7469  ltexprlemdisj  7809  ltexprlemloc  7810  recexprlemdisj  7833  suplocsr  8012  axpre-suploc  8105  nninfdcex  10474  zsupssdc  10475  zfz1isolem1  11080  climmo  11830  summodc  11915  nninfct  12583  ctiunct  13032  ismnd  13473  dfgrp3me  13654  issubg2m  13747  subrgintm  14228  islssm  14342  islidlm  14464  neipsm  14849  suplociccex  15320  bdbm1.3ii  16363