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

Theorem cbvrex 3317
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 2913 . 2 𝑥𝐴
2 nfcv 2913 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexf 3315 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1856  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067
This theorem is referenced by:  cbvrmo  3319  cbvrexv  3321  cbvrexsv  3332  reu8nf  3665  cbviun  4691  isarep1  6117  elabrex  6644  onminex  7154  boxcutc  8105  indexfi  8430  wdom2d  8641  hsmexlem2  9451  fprodle  14933  iundisj  23536  mbfsup  23651  iundisjf  29740  iundisjfi  29895  voliune  30632  volfiniune  30633  bnj1542  31265  cvmcov  31583  poimirlem24  33766  poimirlem26  33768  indexa  33860  rexrabdioph  37884  rexfrabdioph  37885  elabrexg  39728  dffo3f  39884  disjrnmpt2  39895  fvelimad  39976  limsuppnfd  40452  climinf2  40457  limsuppnf  40461  limsupre2  40475  limsupre3  40483  limsupre3uz  40486  limsupreuz  40487  liminfreuz  40553  stoweidlem31  40765  stoweidlem59  40793  meaiunincf  41217  rexsb  41688  cbvrex2  41693
  Copyright terms: Public domain W3C validator