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

Theorem cbvexv 1811
 Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvexv (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexv
StepHypRef Expression
1 ax-17 1435 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-17 1435 . 2 (𝜓 → ∀𝑥𝜓)
3 cbvalv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvexh 1654 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102  ∃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 This theorem is referenced by:  eujust  1918  euind  2751  reuind  2767  r19.3rm  3338  r19.9rmv  3341  raaanlem  3354  raaan  3355  cbvopab2v  3862  bm1.3ii  3906  mss  3990  zfun  4199  xpiindim  4501  relop  4514  dmmrnm  4582  dmxpm  4583  dmcoss  4629  xpm  4773  cnviinm  4887  fv3  5225  fo1stresm  5816  fo2ndresm  5817  iinerm  6209  riinerm  6210  ac6sfi  6383  ltexprlemdisj  6762  ltexprlemloc  6763  recexprlemdisj  6786  climmo  10050  bdbm1.3ii  10398
 Copyright terms: Public domain W3C validator