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

Theorem cbvrex 3307
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 2902 . 2 𝑥𝐴
2 nfcv 2902 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexf 3305 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1857  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056
This theorem is referenced by:  cbvrmo  3309  cbvrexv  3311  cbvrexsv  3322  reu8nf  3657  cbviun  4709  isarep1  6138  elabrex  6664  onminex  7172  boxcutc  8117  indexfi  8439  wdom2d  8650  hsmexlem2  9441  fprodle  14926  iundisj  23516  mbfsup  23630  iundisjf  29709  iundisjfi  29864  voliune  30601  volfiniune  30602  bnj1542  31234  cvmcov  31552  poimirlem24  33746  poimirlem26  33748  indexa  33841  rexrabdioph  37860  rexfrabdioph  37861  elabrexg  39705  dffo3f  39863  disjrnmpt2  39874  fvelimad  39957  limsuppnfd  40437  climinf2  40442  limsuppnf  40446  limsupre2  40460  limsupre3  40468  limsupre3uz  40471  limsupreuz  40472  liminfreuz  40538  stoweidlem31  40751  stoweidlem59  40779  meaiunincf  41203  rexsb  41674  cbvrex2  41679
  Copyright terms: Public domain W3C validator