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

Theorem cbvex 1729
 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 1499 . 2 (𝜑 → ∀𝑦𝜑)
3 cbvex.2 . . 3 𝑥𝜓
43nfri 1499 . 2 (𝜓 → ∀𝑥𝜓)
5 cbvex.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvexh 1728 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  Ⅎwnf 1436  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  sb8e  1829  cbvex2  1894  cbvmo  2039  mo23  2040  clelab  2265  cbvrexf  2649  issetf  2693  eqvincf  2810  rexab2  2850  cbvrexcsf  3063  abn0m  3388  rabn0m  3390  euabsn  3593  eluniab  3748  cbvopab1  4001  cbvopab2  4002  cbvopab1s  4003  intexabim  4077  iinexgm  4079  opeliunxp  4594  dfdmf  4732  dfrnf  4780  elrnmpt1  4790  cbvoprab1  5843  cbvoprab2  5844  opabex3d  6019  opabex3  6020  seq3f1olemp  10275  fsum2dlemstep  11203  bdsepnfALT  13087  strcollnfALT  13184
 Copyright terms: Public domain W3C validator