Theorem cbvexv 1945

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

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

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2059  euind  2970  reuind  2988  r19.2m  3558  r19.3rm  3560  r19.9rmv  3563  raaanlem  3576  raaan  3577  cbvopab2v  4140  bm1.3ii  4184  mss  4291  zfun  4502  xpiindim  4836  relop  4849  dmmrnm  4919  dmxpm  4920  dmcoss  4970  xpm  5126  cnviinm  5246  iotam  5286  fv3  5626  elfvm  5636  fo1stresm  6277  fo2ndresm  6278  tfr1onlemaccex  6464  tfrcllemaccex  6477  iinerm  6724  riinerm  6725  ixpiinm  6841  ac6sfi  7028  ctmlemr  7243  ctm  7244  ctssdclemr  7247  ctssdc  7248  fodjum  7281  finacn  7354  acfun  7357  ccfunen  7418  cc2lem  7420  cc2  7421  ltexprlemdisj  7761  ltexprlemloc  7762  recexprlemdisj  7785  suplocsr  7964  axpre-suploc  8057  nninfdcex  10424  zsupssdc  10425  zfz1isolem1  11029  climmo  11775  summodc  11860  nninfct  12528  ctiunct  12977  ismnd  13418  dfgrp3me  13599  issubg2m  13692  subrgintm  14172  islssm  14286  islidlm  14408  neipsm  14793  suplociccex  15264  bdbm1.3ii  16164