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

Theorem cbvex 2308
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 1824 . . . 4 𝑦 ¬ 𝜑
3 cbval.2 . . . . 5 𝑥𝜓
43nfn 1824 . . . 4 𝑥 ¬ 𝜓
5 cbval.3 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 307 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbval 2307 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 309 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1745 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1745 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 292 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wal 1521  wex 1744  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  cbvexvOLD  2312  sb8e  2453  exsb  2496  euf  2506  mo2  2507  cbvmo  2535  clelab  2777  issetf  3239  eqvincf  3362  rexab2  3406  euabsn  4293  eluniab  4479  cbvopab1  4756  cbvopab2  4757  cbvopab1s  4758  axrep1  4805  axrep2  4806  axrep4  4808  opeliunxp  5204  dfdmf  5349  dfrnf  5396  elrnmpt1  5406  cbvoprab1  6769  cbvoprab2  6770  opabex3d  7187  opabex3  7188  zfcndrep  9474  fsum2dlem  14545  fprod2dlem  14754  bnj1146  30988  bnj607  31112  bnj1228  31205  poimirlem26  33565  sbcexf  34048  elunif  39489  stoweidlem46  40581  opeliun2xp  42436
  Copyright terms: Public domain W3C validator