Theorem cbvralv 2726

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralv	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralv

Step	Hyp	Ref	Expression
1		nfv 1539	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1539	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2722	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477

This theorem is referenced by:  cbvral2v  2739  cbvral3v  2741  reu7  2955  reusv3i  4490  omsinds  4654  cnvpom  5208  f1mpt  5814  tfrlem1  6361  tfrlemiubacc  6383  tfrlemi1  6385  tfr1onlemubacc  6399  tfr1onlemaccex  6401  tfrcllembxssdm  6409  tfrcllemubacc  6412  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  rdgon  6439  frecfcllem  6457  frecsuclem  6459  nneneq  6913  fimax2gtrilemstep  6956  supubti  7058  suplubti  7059  finomni  7199  nninfwlporlemd  7231  acfun  7267  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  ccfunen  7324  cc2  7327  cauappcvgprlemladdrl  7717  caucvgprlemcl  7736  caucvgprlemladdrl  7738  caucvgsrlembound  7854  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  suplocsrlem  7868  peano5nnnn  7952  axcaucvglemres  7959  axpre-suploc  7962  suprleubex  8973  nnsub  9021  supinfneg  9660  infsupneg  9661  infregelbex  9663  ublbneg  9678  exbtwnzlemex  10318  uzsinds  10515  iseqovex  10529  seq3val  10531  seqvalcd  10532  seqf  10535  seqovcd  10538  monoord2  10557  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seq3f1olemqsum  10584  seq3f1olemp  10586  seq3f1oleml  10587  seq3f1o  10588  nn0ltexp2  10780  bccl  10838  seq3shft  10982  caucvgre  11125  cvg1nlemcau  11128  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  cau3lem  11258  zsumdc  11527  fsum3  11530  isumz  11532  isumss2  11536  fsumsersdc  11538  fsum3ser  11540  fisum0diag2  11590  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratz  11675  mertenslem2  11679  mertensabs  11680  zproddc  11722  fprodseq  11726  prod1dc  11729  fprodsplitdc  11739  zsupssdc  12091  bezoutlemmain  12135  bezoutlemex  12138  bezoutlemzz  12139  bezoutlemeu  12144  bezoutlemle  12145  dfgcd3  12147  prmind2  12258  sqrt2irr  12300  hashdvds  12359  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemr  12580  ctinfom  12585  ctinf  12587  ctiunctlemudc  12594  ssnnctlemct  12603  nninfdclemp1  12607  tgcn  14376  mulcncflem  14761  suplociccreex  14778  dedekindicc  14787  nnsf  15495  nninfsellemqall  15505  nninfomni  15509  trirec0  15534  apdiff  15538  iswomni0  15541  dceqnconst  15550  dcapnconst  15551  neap0mkv  15559  ltlenmkv  15560