Theorem cbvrexv 1804

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 973	. 2 |- (ph -> A.yph)
2		ax-17 973	. 2 |- (ps -> A.xps)
3		cbvralv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbvrex 1802	1 |- (E.x e. A ph <-> E.y e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958  E.wrex 1649

This theorem is referenced by:  reu7 1938  dffr2 2925  funcnvuni 3570  tfrlem3 3919  abianfp 3968  nneob 4261  php3OLD 4522  ominfOLD 4537  pssnn 4544  ssfiOLD 4548  unfiOLD 4564  unifiOLD 4570  fodomfiOLD 4576  pwfiOLD 4580  trcl 4655  r1pwcl 4697  aceq2 4741  aceq5lem4 4748  kmlem9 4783  kmlem14 4788  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  fsequb 6524  creur 6743  creui 6744  seq1bnd 6910  cau3ir 6915  cau5i 6917  cvg1 6921  cvg3 6923  cvganz 6924  clm3 7079  caucvg3t 7168  subtop 7643  grpidinvlem3 8047  isgrp2i 8072  minvecex 8574  efghgrpilem 8714  axgroth4 8775  axhcompl 8863  norm1ex 9117  projlem15 9195  pjtheu 9230  lnfncon 9985  cdjreu 10354  cdj3 10363  fgsb 10555  fgsb2 10560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475  df-rex 1653

Copyright terms: Public domain