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

Theorem cbvex 1686
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 1457 . 2 (𝜑 → ∀𝑦𝜑)
3 cbvex.2 . . 3 𝑥𝜓
43nfri 1457 . 2 (𝜓 → ∀𝑥𝜓)
5 cbvex.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
62, 4, 5cbvexh 1685 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wnf 1394  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  sb8e  1785  cbvex2  1845  cbvmo  1988  mo23  1989  clelab  2212  cbvrexf  2585  issetf  2626  eqvincf  2742  rexab2  2781  cbvrexcsf  2991  abn0m  3308  rabn0m  3310  euabsn  3512  eluniab  3665  cbvopab1  3911  cbvopab2  3912  cbvopab1s  3913  intexabim  3988  iinexgm  3990  opeliunxp  4493  dfdmf  4629  dfrnf  4676  elrnmpt1  4686  cbvoprab1  5720  cbvoprab2  5721  opabex3d  5892  opabex3  5893  seq3f1olemp  9931  fsum2dlemstep  10828  bdsepnfALT  11780  strcollnfALT  11881
  Copyright terms: Public domain W3C validator