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

Theorem cbvexv 1840
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 1462 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-17 1462 . 2 (𝜓 → ∀𝑥𝜓)
3 cbvalv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvexh 1682 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wex 1424
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eujust  1947  euind  2793  reuind  2809  r19.3rm  3357  r19.9rmv  3360  raaanlem  3374  raaan  3375  cbvopab2v  3892  bm1.3ii  3937  mss  4029  zfun  4237  xpiindim  4543  relop  4556  dmmrnm  4625  dmxpm  4626  dmcoss  4672  xpm  4821  cnviinm  4940  fv3  5293  fo1stresm  5891  fo2ndresm  5892  tfr1onlemaccex  6069  tfrcllemaccex  6082  iinerm  6318  riinerm  6319  ac6sfi  6568  fodjuomnilemm  6748  ltexprlemdisj  7112  ltexprlemloc  7113  recexprlemdisj  7136  zfz1isolem1  10163  climmo  10602  isummo  10686  bdbm1.3ii  11270
  Copyright terms: Public domain W3C validator