Theorem cbvexv 1974

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  eujust  2088  euind  3013  reuind  3031  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  cbvopab2v  4209  bm1.3ii  4256  mss  4368  zfun  4581  xpiindim  4919  relop  4932  reldmm  5002  dmmrnm  5003  dmxpm  5004  dmcoss  5054  xpm  5212  cnviinm  5332  iotam  5372  fv3  5721  elfvm  5732  mptmex  5948  fo1stresm  6399  fo2ndresm  6400  tfr1onlemaccex  6623  tfrcllemaccex  6636  iinerm  6885  riinerm  6886  ixpiinm  7011  ac6sfi  7207  ctmlemr  7455  ctm  7456  ctssdclemr  7459  ctssdc  7460  fodjum  7493  finacn  7567  acfun  7570  ccfunen  7637  cc2lem  7639  cc2  7640  ltexprlemdisj  7980  ltexprlemloc  7981  recexprlemdisj  8004  suplocsr  8183  axpre-suploc  8276  nninfdcex  10690  zsupssdc  10691  zfz1isolem1  11315  climmo  12090  summodc  12176  nninfct  12844  ctiunct  13390  ismnd  13792  dfgrp3me  13965  issubg2m  14052  gsumvalfi  14243  subrgintm  14661  islssm  14804  islidlm  14926  neipsm  15392  suplociccex  15863  bdbm1.3ii  17134