Theorem cbvralv 2703

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 1528	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1528	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 2699	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  cbvral2v  2716  cbvral3v  2718  reu7  2932  reusv3i  4459  omsinds  4621  cnvpom  5171  f1mpt  5771  tfrlem1  6308  tfrlemiubacc  6330  tfrlemi1  6332  tfr1onlemubacc  6346  tfr1onlemaccex  6348  tfrcllembxssdm  6356  tfrcllemubacc  6359  tfrcllemaccex  6361  tfrcllemres  6362  tfrcldm  6363  rdgon  6386  frecfcllem  6404  frecsuclem  6406  nneneq  6856  fimax2gtrilemstep  6899  supubti  6997  suplubti  6998  finomni  7137  nninfwlporlemd  7169  acfun  7205  exmidontriimlem3  7221  exmidontriimlem4  7222  exmidontriim  7223  ccfunen  7262  cc2  7265  cauappcvgprlemladdrl  7655  caucvgprlemcl  7674  caucvgprlemladdrl  7676  caucvgsrlembound  7792  caucvgsrlemgt1  7793  caucvgsrlemoffres  7798  suplocsrlem  7806  peano5nnnn  7890  axcaucvglemres  7897  axpre-suploc  7900  suprleubex  8910  nnsub  8957  supinfneg  9594  infsupneg  9595  infregelbex  9597  ublbneg  9612  exbtwnzlemex  10249  uzsinds  10441  iseqovex  10455  seq3val  10457  seqvalcd  10458  seqf  10460  seqovcd  10462  monoord2  10476  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  seq3f1olemqsum  10499  seq3f1olemp  10501  seq3f1oleml  10502  seq3f1o  10503  nn0ltexp2  10688  bccl  10746  seq3shft  10846  caucvgre  10989  cvg1nlemcau  10992  resqrexlemglsq  11030  resqrexlemsqa  11032  resqrexlemex  11033  cau3lem  11122  zsumdc  11391  fsum3  11394  isumz  11396  isumss2  11400  fsumsersdc  11402  fsum3ser  11404  fisum0diag2  11454  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratz  11539  mertenslem2  11543  mertensabs  11544  zproddc  11586  fprodseq  11590  prod1dc  11593  fprodsplitdc  11603  zsupssdc  11954  bezoutlemmain  11998  bezoutlemex  12001  bezoutlemzz  12002  bezoutlemeu  12007  bezoutlemle  12008  dfgcd3  12010  prmind2  12119  sqrt2irr  12161  hashdvds  12220  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemr  12423  ctinfom  12428  ctinf  12430  ctiunctlemudc  12437  ssnnctlemct  12446  nninfdclemcl  12448  nninfdclemp1  12450  tgcn  13678  mulcncflem  14060  suplociccreex  14072  dedekindicc  14081  nnsf  14724  nninfsellemqall  14734  nninfomni  14738  trirec0  14762  apdiff  14766  iswomni0  14769  dceqnconst  14777  dcapnconst  14778  neap0mkv  14786  ltlenmkv  14787