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  4312  zfun  4525  xpiindim  4859  relop  4872  reldmm  4942  dmmrnm  4943  dmxpm  4944  dmcoss  4994  xpm  5150  cnviinm  5270  iotam  5310  fv3  5652  elfvm  5662  fo1stresm  6313  fo2ndresm  6314  tfr1onlemaccex  6500  tfrcllemaccex  6513  iinerm  6762  riinerm  6763  ixpiinm  6879  ac6sfi  7068  ctmlemr  7283  ctm  7284  ctssdclemr  7287  ctssdc  7288  fodjum  7321  finacn  7394  acfun  7397  ccfunen  7458  cc2lem  7460  cc2  7461  ltexprlemdisj  7801  ltexprlemloc  7802  recexprlemdisj  7825  suplocsr  8004  axpre-suploc  8097  nninfdcex  10465  zsupssdc  10466  zfz1isolem1  11070  climmo  11817  summodc  11902  nninfct  12570  ctiunct  13019  ismnd  13460  dfgrp3me  13641  issubg2m  13734  subrgintm  14215  islssm  14329  islidlm  14451  neipsm  14836  suplociccex  15307  bdbm1.3ii  16278