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

Theorem cbvrex 3144
 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 2751 . 2 𝑥𝐴
2 nfcv 2751 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrexf 3142 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902 This theorem is referenced by:  cbvrmo  3146  cbvrexv  3148  cbvrexsv  3159  cbviun  4493  isarep1  5891  elabrex  6405  onminex  6899  boxcutc  7837  indexfi  8157  wdom2d  8368  hsmexlem2  9132  fprodle  14566  iundisj  23123  mbfsup  23237  iundisjf  28784  iundisjfi  28942  voliune  29619  volfiniune  29620  bnj1542  30181  cvmcov  30499  poimirlem24  32603  poimirlem26  32605  indexa  32698  rexrabdioph  36376  rexfrabdioph  36377  elabrexg  38229  dffo3f  38359  disjrnmpt2  38370  stoweidlem31  38924  stoweidlem59  38952  rexsb  39817  cbvrex2  39822
 Copyright terms: Public domain W3C validator