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

Theorem cbvex 2259
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
cbval.1 𝑦𝜑
cbval.2 𝑥𝜓
cbval.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvex (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Proof of Theorem cbvex
StepHypRef Expression
1 cbval.1 . . . . 5 𝑦𝜑
21nfn 1767 . . . 4 𝑦 ¬ 𝜑
3 cbval.2 . . . . 5 𝑥𝜓
43nfn 1767 . . . 4 𝑥 ¬ 𝜓
5 cbval.3 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 306 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbval 2258 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 308 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1695 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1695 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 290 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wal 1472  wex 1694  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by:  cbvexvOLD  2263  sb8e  2412  exsb  2455  euf  2465  mo2  2466  cbvmo  2493  clelab  2734  issetf  3180  eqvincf  3300  rexab2  3339  euabsn  4204  eluniab  4377  cbvopab1  4649  cbvopab2  4650  cbvopab1s  4651  axrep1  4694  axrep2  4695  axrep4  4697  opeliunxp  5082  dfdmf  5225  dfrnf  5271  elrnmpt1  5281  cbvoprab1  6602  cbvoprab2  6603  opabex3d  7014  opabex3  7015  zfcndrep  9292  fsum2dlem  14291  fprod2dlem  14497  bnj1146  29909  bnj607  30033  bnj1228  30126  poimirlem26  32388  sbcexf  32871  elunif  37981  stoweidlem46  38722  opeliun2xp  41885
  Copyright terms: Public domain W3C validator