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

Theorem cbvexv 1891
 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 1507 . 2 (𝜑 → ∀𝑦𝜑)
2 ax-17 1507 . 2 (𝜓 → ∀𝑥𝜓)
3 cbvalv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvexh 1729 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1469 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  cbvexvw  1893  eujust  2002  euind  2874  reuind  2892  r19.2m  3453  r19.3rm  3455  r19.9rmv  3458  raaanlem  3472  raaan  3473  cbvopab2v  4012  bm1.3ii  4056  mss  4155  zfun  4363  xpiindim  4683  relop  4696  dmmrnm  4765  dmxpm  4766  dmcoss  4815  xpm  4967  cnviinm  5087  fv3  5451  fo1stresm  6066  fo2ndresm  6067  tfr1onlemaccex  6252  tfrcllemaccex  6265  iinerm  6508  riinerm  6509  ixpiinm  6625  ac6sfi  6799  ctmlemr  7000  ctm  7001  ctssdclemr  7004  ctssdc  7005  fodjum  7025  acfun  7079  ccfunen  7095  cc2lem  7097  cc2  7098  ltexprlemdisj  7437  ltexprlemloc  7438  recexprlemdisj  7461  suplocsr  7640  axpre-suploc  7733  zfz1isolem1  10614  climmo  11098  summodc  11183  ctiunct  11987  neipsm  12360  suplociccex  12809  bdbm1.3ii  13258
 Copyright terms: Public domain W3C validator