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

Theorem cbvex 1639
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 1412 . 2 (𝜑 → ∀𝑦𝜑)
3 cbvex.2 . . 3 𝑥𝜓
43nfri 1412 . 2 (𝜓 → ∀𝑥𝜓)
5 cbvex.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvexh 1638 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1349  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-nf 1350
This theorem is referenced by:  sb8e  1737  cbvex2  1797  cbvmo  1940  mo23  1941  clelab  2162  cbvrexf  2528  issetf  2562  eqvincf  2669  rexab2  2707  cbvrexcsf  2909  rabn0m  3245  euabsn  3440  eluniab  3592  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  intexabim  3906  iinexgm  3908  opeliunxp  4395  dfdmf  4528  dfrnf  4575  elrnmpt1  4585  cbvoprab1  5576  cbvoprab2  5577  opabex3d  5748  opabex3  5749  bdsepnfALT  9983  strcollnfALT  10085
  Copyright terms: Public domain W3C validator