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

Theorem cbvex 2271
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 1781 . . . 4 𝑦 ¬ 𝜑
3 cbval.2 . . . . 5 𝑥𝜓
43nfn 1781 . . . 4 𝑥 ¬ 𝜓
5 cbval.3 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 308 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbval 2270 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 310 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1702 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1702 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 292 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wal 1478  wex 1701  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  cbvexvOLD  2275  sb8e  2424  exsb  2467  euf  2477  mo2  2478  cbvmo  2505  clelab  2745  issetf  3198  eqvincf  3319  rexab2  3360  euabsn  4238  eluniab  4420  cbvopab1  4695  cbvopab2  4696  cbvopab1s  4697  axrep1  4742  axrep2  4743  axrep4  4745  opeliunxp  5141  dfdmf  5287  dfrnf  5334  elrnmpt1  5344  cbvoprab1  6692  cbvoprab2  6693  opabex3d  7106  opabex3  7107  zfcndrep  9396  fsum2dlem  14448  fprod2dlem  14654  bnj1146  30623  bnj607  30747  bnj1228  30840  poimirlem26  33106  sbcexf  33589  elunif  38697  stoweidlem46  39600  opeliun2xp  41429
  Copyright terms: Public domain W3C validator