Theorem cbvralv 2786

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  cbvral2v  2799  cbvral3v  2801  reu7  3021  reusv3i  4607  omsinds  4771  cnvpom  5333  f1mpt  5980  tfrlem1  6584  tfrlemiubacc  6606  tfrlemi1  6608  tfr1onlemubacc  6622  tfr1onlemaccex  6624  tfrcllembxssdm  6632  tfrcllemubacc  6635  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  rdgon  6662  frecfcllem  6680  frecsuclem  6682  nneneq  7164  fimax2gtrilemstep  7211  supubti  7345  suplubti  7346  finomni  7486  nninfwlporlemd  7518  nninfinfwlpo  7526  acfun  7569  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  ccfunen  7636  cc2  7639  cauappcvgprlemladdrl  8030  caucvgprlemcl  8049  caucvgprlemladdrl  8051  caucvgsrlembound  8167  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  suplocsrlem  8181  peano5nnnn  8265  axcaucvglemres  8272  axpre-suploc  8275  suprleubex  9292  nnsub  9352  supinfneg  10010  infsupneg  10011  infregelbex  10013  ublbneg  10028  irraddap  10062  zsupssdc  10689  exbtwnzlemex  10700  uzsinds  10901  iseqovex  10915  seq3val  10917  seqvalcd  10918  seqf  10921  seqovcd  10924  monoord2  10943  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1olemqsum  10970  seq3f1olemp  10972  seq3f1oleml  10973  seq3f1o  10974  nn0ltexp2  11168  bccl  11226  seq3shft  11624  caucvgre  11768  cvg1nlemcau  11771  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  cau3lem  11902  zsumdc  12175  fsum3  12178  isumz  12180  isumss2  12184  fsumsersdc  12186  fsum3ser  12188  fisum0diag2  12238  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratz  12323  mertenslem2  12327  mertensabs  12328  zproddc  12370  fprodseq  12374  prod1dc  12377  fprodsplitdc  12387  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemzz  12803  bezoutlemeu  12808  bezoutlemle  12809  dfgcd3  12811  prmind2  12922  sqrt2irr  12965  hashdvds  13027  ballotfilemefi  13294  ballotfilemodife  13297  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemr  13371  ctinfom  13376  ctinf  13378  ctiunctlemudc  13385  ssnnctlemct  13394  nninfdclemp1  13398  psrbaglefifi  15175  psrbagmax  15183  tgcn  15451  mulcncflem  15850  suplociccreex  15867  dedekindicc  15876  vtxedgfi  16752  vtxlpfi  16753  nnsf  17271  nninfsellemqall  17281  nninfomni  17285  repiecef  17300  trirec0  17317  apdiff  17321  iswomni0  17325  dceqnconst  17334  dcapnconst  17335  neap0mkv  17343  ltlenmkv  17344