Theorem cbvrexv 1801

Description: Change the bound variable of a restricted existential quantifier using implicit substitution.

Hypothesis

Ref	Expression
cbvralv.1	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
cbvrexv	|- (E.x e. A ph <-> E.y e. A ps)

Distinct variable groups:   ph,y   ps,x   x,y,A

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ph -> A.yph)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		cbvralv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbvrex 1799	1 |- (E.x e. A ph <-> E.y e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  E.wrex 1646

This theorem is referenced by:  reu7 1935  dffr2 2919  funcnvuni 3564  tfrlem3 3913  abianfp 3962  nneob 4255  php3OLD 4516  ominfOLD 4529  pssnn 4534  ssfiOLD 4538  unfiOLD 4552  unifiOLD 4557  abfii4OLD 4564  fodomfiOLD 4566  pwfiOLD 4571  trcl 4645  r1pwcl 4687  aceq2 4731  aceq5lem4 4738  kmlem9 4773  kmlem14 4778  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  fsequb 6523  creur 6742  creui 6743  seq1bnd 6910  cau3ir 6915  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  clm3 7079  caucvg3t 7168  subtop 7646  grpidinvlem3 8050  isgrp2i 8076  minvecex 8578  efghgrpilem 8719  axgroth4 8780  axhcompl 8868  norm1ex 9122  projlem15 9200  pjtheu 9235  lnfncon 9990  cdjreu 10359  cdj3 10368  fgsb 10570  fgsbOLD 10571  infiOLD 10579  fgsb2 10580  rcfpfillem2OLD 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472  df-rex 1650

Copyright terms: Public domain