Theorem cbvexv 1918

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2028  euind  2925  reuind  2943  r19.2m  3510  r19.3rm  3512  r19.9rmv  3515  raaanlem  3529  raaan  3530  cbvopab2v  4081  bm1.3ii  4125  mss  4227  zfun  4435  xpiindim  4765  relop  4778  dmmrnm  4847  dmxpm  4848  dmcoss  4897  xpm  5051  cnviinm  5171  iotam  5209  fv3  5539  fo1stresm  6162  fo2ndresm  6163  tfr1onlemaccex  6349  tfrcllemaccex  6362  iinerm  6607  riinerm  6608  ixpiinm  6724  ac6sfi  6898  ctmlemr  7107  ctm  7108  ctssdclemr  7111  ctssdc  7112  fodjum  7144  acfun  7206  ccfunen  7263  cc2lem  7265  cc2  7266  ltexprlemdisj  7605  ltexprlemloc  7606  recexprlemdisj  7629  suplocsr  7808  axpre-suploc  7901  zfz1isolem1  10820  climmo  11306  summodc  11391  nninfdcex  11954  zsupssdc  11955  ctiunct  12441  ismnd  12820  dfgrp3me  12970  issubg2m  13049  subrgintm  13364  neipsm  13657  suplociccex  14106  bdbm1.3ii  14646