MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvralv Structured version   Visualization version   GIF version

Theorem cbvralv 3453
Description: Change the bound variable of a restricted universal quantifier using implicit substitution. See cbvralvw 3450 based on fewer axioms , but extra disjoint variables. (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
StepHypRef Expression
1 nfv 1906 . 2 𝑦𝜑
2 nfv 1906 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvral 3446 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2383
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clel 2893  df-nfc 2963  df-ral 3143
This theorem is referenced by:  cbvral2v  3465  cbvral3v  3467  disjxun  5056  frgrwopreglem5ALT  28029  bnj1452  32222  poimirlem27  34801  disjinfi  41334  limsupubuz  41874  limsupmnf  41882  limsupre2  41886  limsupmnfuz  41888  limsupre2mpt  41891  limsupre3  41894  limsupre3mpt  41895  limsupre3uzlem  41896  limsupre3uz  41897  limsupreuz  41898  limsupvaluz2  41899  limsupreuzmpt  41900  climuz  41905  lmbr3  41908  liminfreuz  41964  xlimpnfxnegmnf  41975  xlimmnf  42002  xlimpnf  42003  xlimmnfmpt  42004  xlimpnfmpt  42005  dfxlim2  42009  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnprodlem3  42113  wallispilem3  42233  fourierdlem68  42340  fourierdlem71  42343  fourierdlem73  42345  fourierdlem87  42359  fourierdlem100  42372  fourierdlem103  42375  fourierdlem104  42376  fourierdlem107  42379  fourierdlem109  42381  fourierdlem112  42384  etransc  42449  qndenserrnbllem  42460  dfsalgen2  42505  subsaliuncl  42522  meaiuninclem  42643  ovnsubaddlem2  42734  hoidmvlelem5  42762  hoidmvle  42763  hoiqssbllem3  42787  vonioo  42845  vonicc  42848  issmf  42886  issmfle  42903  issmfgt  42914  issmfge  42927  smfsuplem2  42967  2reuimp0  43194  sbgoldbm  43796  mogoldbb  43797  bgoldbtbndlem4  43820  bgoldbtbnd  43821  nn0sumshdiglem1  44579
  Copyright terms: Public domain W3C validator