Theorem cbvralv 2280

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,A   y,A

Proof of Theorem cbvralv

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

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  A.wral 2105

This theorem is referenced by:  cbvral2v 2283  cbvral3v 2284  reu7 2447  dfwe2 3861  dfwe2OLD 3862  tfindsOLD 3943  cnvpo 4427  tfrlem1 5119  rdglem1 5145  tz7.48lem 5164  nneneq 5606  supmo 5666  supmaxlem 5678  ordtype 5691  aceq1 5891  aceq2 5893  aceq5 5902  kmlem12 5938  kmlem14 5940  zorn2lem7 5956  zorn2 5958  nnleltp1 7138  xrub 7289  supxrre 7292  zindd 7427  uzwo3lem2 7430  uzwo3 7431  uzwo 7624  uzwoOLD 7625  fsequb 7702  sqr2irrlem3 7976  cau3iri 8167  cvg2i 8174  faclbnd4lem4 8203  bccl2 8223  caucvg3 8428  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isum1p 8467  isummulc1iALT 8474  negfcncfi 8531  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  elcls3 8987  grpideu 9333  ubthlem1 9872  spwmo 9999  sincolem 10014  pilem2 10021  grothomex 10136  axgroth6 10137  exidu1 10373  hlimcauii 10739  adjsym 11396  lnopunilem1 11572  elunop2 11575  lnophm 11581  lnopconi 11600  cnlnadjlem5 11641  mdbr3 11869  mdbr4 11870  dmdbr3 11877  dmdbr4 11878  mddmd2 11881  bnj39 12410  bnj1379 13100  bnj222 13251  bnj589 13297  bnj1450 13541  bnj1462 13546  bnj1463 13550  cayleylem2 13642  ublbneg 13653  gcdcllem1 13718  untangtr 13802  dfon2lem3 13851  dfon2lem7 13855  cbvsetlike 13892  wfrlem1 13957  tfr3ALT 13979  axfelem15 14045  celsor 14443  curgrpact 14735  cntrsetlem 14999  taralt 15211  btmp 15252  ordtypeOLD 15382  alexsublem2 15438  alexsublem4 15440  neibastop2lem3 15521  upixp 15729  fimax 15746  frfi 15771  sdclem1 15809  sdc 15811  fdc 15812  fsumleisumi 15826  mettrifi 15847  heiborlem31 15985  grpideuNEW 17114

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-cleq 1877  df-clel 1880  df-ral 2109

Copyright terms: Public domain