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

Theorem cbvrex 3373
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 2925 . 2 𝑥𝐴
2 nfcv 2925 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexf 3371 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wnf 1747  wrex 3082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087
This theorem is referenced by:  cbvrmo  3375  cbvrexv  3377  cbvrexsv  3389  reu8nf  3756  cbviun  4827  isarep1  6272  fvelimad  6559  elabrex  6825  onminex  7336  boxcutc  8300  indexfi  8625  wdom2d  8837  hsmexlem2  9645  fprodle  15208  iundisj  23867  mbfsup  23983  iundisjf  30122  iundisjfi  30292  voliune  31165  volfiniune  31166  bnj1542  31808  cvmcov  32132  poimirlem24  34394  poimirlem26  34396  indexa  34487  rexrabdioph  38825  rexfrabdioph  38826  elabrexg  40760  dffo3f  40897  disjrnmpt2  40908  limsuppnfd  41448  climinf2  41453  limsuppnf  41457  limsupre2  41471  limsupre3  41479  limsupre3uz  41482  limsupreuz  41483  liminfreuz  41549  stoweidlem31  41781  stoweidlem59  41809  meaiunincf  42230  rexsb  42737  cbvrex2  42742  2reu8i  42752
  Copyright terms: Public domain W3C validator