Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvex GIF version

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

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . 3 𝑦𝜑
21nfri 1428 . 2 (𝜑 → ∀𝑦𝜑)
3 cbvex.2 . . 3 𝑥𝜓
43nfri 1428 . 2 (𝜓 → ∀𝑥𝜓)
5 cbvex.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvexh 1654 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102  Ⅎwnf 1365  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443 This theorem depends on definitions:  df-bi 114  df-nf 1366 This theorem is referenced by:  sb8e  1753  cbvex2  1813  cbvmo  1956  mo23  1957  clelab  2178  cbvrexf  2545  issetf  2579  eqvincf  2692  rexab2  2730  cbvrexcsf  2937  rabn0m  3273  euabsn  3468  eluniab  3620  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  intexabim  3934  iinexgm  3936  opeliunxp  4423  dfdmf  4556  dfrnf  4603  elrnmpt1  4613  cbvoprab1  5604  cbvoprab2  5605  opabex3d  5776  opabex3  5777  bdsepnfALT  10396  strcollnfALT  10498
 Copyright terms: Public domain W3C validator