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 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 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 theorem 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 referenced by:  cbvral2v  2799  cbvral3v  2801  reu7  3021  reusv3i  4600  omsinds  4764  cnvpom  5325  f1mpt  5967  tfrlem1  6569  tfrlemiubacc  6591  tfrlemi1  6593  tfr1onlemubacc  6607  tfr1onlemaccex  6609  tfrcllembxssdm  6617  tfrcllemubacc  6620  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  rdgon  6647  frecfcllem  6665  frecsuclem  6667  nneneq  7148  fimax2gtrilemstep  7195  supubti  7329  suplubti  7330  finomni  7470  nninfwlporlemd  7502  nninfinfwlpo  7510  acfun  7553  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  ccfunen  7620  cc2  7623  cauappcvgprlemladdrl  8014  caucvgprlemcl  8033  caucvgprlemladdrl  8035  caucvgsrlembound  8151  caucvgsrlemgt1  8152  caucvgsrlemoffres  8157  suplocsrlem  8165  peano5nnnn  8249  axcaucvglemres  8256  axpre-suploc  8259  suprleubex  9274  nnsub  9322  supinfneg  9974  infsupneg  9975  infregelbex  9977  ublbneg  9992  zsupssdc  10651  exbtwnzlemex  10662  uzsinds  10859  iseqovex  10873  seq3val  10875  seqvalcd  10876  seqf  10879  seqovcd  10882  monoord2  10901  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seq3f1olemqsum  10928  seq3f1olemp  10930  seq3f1oleml  10931  seq3f1o  10932  nn0ltexp2  11125  bccl  11183  seq3shft  11581  caucvgre  11725  cvg1nlemcau  11728  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  cau3lem  11858  zsumdc  12129  fsum3  12132  isumz  12134  isumss2  12138  fsumsersdc  12140  fsum3ser  12142  fisum0diag2  12192  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratz  12277  mertenslem2  12281  mertensabs  12282  zproddc  12324  fprodseq  12328  prod1dc  12331  fprodsplitdc  12341  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemzz  12757  bezoutlemeu  12762  bezoutlemle  12763  dfgcd3  12765  prmind2  12876  sqrt2irr  12918  hashdvds  12977  ballotfilemefi  13215  ballotfilemodife  13218  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemr  13292  ctinfom  13297  ctinf  13299  ctiunctlemudc  13306  ssnnctlemct  13315  nninfdclemp1  13319  mplsubgfilemcl  15013  tgcn  15232  mulcncflem  15631  suplociccreex  15648  dedekindicc  15657  vtxedgfi  16444  vtxlpfi  16445  nnsf  16953  nninfsellemqall  16963  nninfomni  16967  repiecef  16982  trirec0  16998  apdiff  17002  iswomni0  17006  dceqnconst  17015  dcapnconst  17016  neap0mkv  17024  ltlenmkv  17025