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

Theorem cbvrex 3156
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Hypotheses
Ref Expression
cbvral.1 𝑦𝜑
cbvral.2 𝑥𝜓
cbvral.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrex (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvrex
StepHypRef Expression
1 nfcv 2761 . 2 𝑥𝐴
2 nfcv 2761 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexf 3154 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1705  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913
This theorem is referenced by:  cbvrmo  3158  cbvrexv  3160  cbvrexsv  3171  cbviun  4525  isarep1  5937  elabrex  6458  onminex  6957  boxcutc  7898  indexfi  8221  wdom2d  8432  hsmexlem2  9196  fprodle  14655  iundisj  23229  mbfsup  23344  iundisjf  29259  iundisjfi  29408  voliune  30085  volfiniune  30086  bnj1542  30656  cvmcov  30974  poimirlem24  33086  poimirlem26  33088  indexa  33181  rexrabdioph  36859  rexfrabdioph  36860  elabrexg  38710  dffo3f  38856  disjrnmpt2  38867  fvelimad  38951  limsuppnfd  39356  climinf2  39361  limsuppnf  39365  limsupre2  39379  limsupre3  39387  limsupre3uz  39390  limsupreuz  39391  stoweidlem31  39571  stoweidlem59  39599  rexsb  40488  cbvrex2  40493
  Copyright terms: Public domain W3C validator