Theorem cbvralv 1791

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

Hypothesis

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

Assertion

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

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

Proof of Theorem cbvralv

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953  A.wral 1637

This theorem is referenced by:  cbvral2v 1794  cbvral3v 1795  reu7 1925  dfwe2 2925  tfinds 3151  cnvpo 3508  tfrlem1 3896  rdglem1 3922  tz7.48lem 3940  nneneq 4492  supmo 4550  aceq1 4701  aceq2 4703  aceq5 4712  kmlem12 4748  kmlem14 4750  zorn2lem7 4766  zorn2 4768  nnleltp1t 5901  xrub 6027  supxrre 6030  uzwo3lem2 6165  uzwo3 6166  uzwo 6387  uzwoOLD 6388  fsequb 6455  sqr2irrlem3 6656  cau3ir 6852  cvg2 6859  faclbnd4lem4 6888  bccl2t 6909  caucvg3t 7104  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  isum1p 7141  isummulc1ALT 7148  negfcncf 7204  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  elcls3 7652  grpideu 7987  ubthlem1 8460  spwmo 8580  sincolem 8584  pilem2 8591  grothinf 8720  hlimcaui 9027  adjsymt 9676  lnopunilem1 9850  elunop2t 9853  lnophmt 9859  lnopcon 9878  cnlnadjlem5 9919  mdbr3 10134  mdbr4 10135  dmdbr3 10141  dmdbr4 10142  mddmd 10144  cayleylem2 10317

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465  df-ral 1641

Copyright terms: Public domain