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

Theorem cbvex 1736
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 1735 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wnf 1440  wex 1472
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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514
This theorem depends on definitions:  df-bi 116  df-nf 1441
This theorem is referenced by:  sb8e  1837  cbvex2  1902  cbvmo  2046  mo23  2047  clelab  2283  cbvrexf  2675  issetf  2719  eqvincf  2837  rexab2  2878  cbvrexcsf  3094  abn0m  3419  rabn0m  3421  euabsn  3629  eluniab  3784  cbvopab1  4037  cbvopab2  4038  cbvopab1s  4039  intexabim  4113  iinexgm  4115  opeliunxp  4641  dfdmf  4779  dfrnf  4827  elrnmpt1  4837  cbvoprab1  5893  cbvoprab2  5894  opabex3d  6069  opabex3  6070  seq3f1olemp  10401  fsum2dlemstep  11331  bdsepnfALT  13475  strcollnfALT  13572
  Copyright terms: Public domain W3C validator