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

Theorem cbvex 2417
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 1933 . . . 4 𝑦 ¬ 𝜑
3 cbval.2 . . . . 5 𝑥𝜓
43nfn 1933 . . . 4 𝑥 ¬ 𝜓
5 cbval.3 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 307 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbval 2416 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 309 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1854 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1854 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 292 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wal 1630  wex 1853  wnf 1857
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-ex 1854  df-nf 1859
This theorem is referenced by:  cbvexvOLD  2421  sb8e  2562  exsb  2605  euf  2615  mo2  2616  cbvmo  2644  clelab  2886  issetf  3348  eqvincf  3470  rexab2  3514  euabsn  4405  eluniab  4599  cbvopab1  4875  cbvopab2  4876  cbvopab1s  4877  axrep1  4924  axrep2  4925  axrep4  4927  opeliunxp  5327  dfdmf  5472  dfrnf  5519  elrnmpt1  5529  cbvoprab1  6892  cbvoprab2  6893  opabex3d  7310  opabex3  7311  zfcndrep  9628  fsum2dlem  14700  fprod2dlem  14909  bnj1146  31169  bnj607  31293  bnj1228  31386  poimirlem26  33748  sbcexf  34231  elunif  39674  stoweidlem46  40766  opeliun2xp  42621
  Copyright terms: Public domain W3C validator