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

Theorem cbvral 2655
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
Hypotheses
Ref Expression
cbvral.1
cbvral.2
cbvral.3
Assertion
Ref Expression
cbvral
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   (,)

Proof of Theorem cbvral
StepHypRef Expression
1 nfcv 2283 . 2
2 nfcv 2283 . 2
3 cbvral.1 . 2
4 cbvral.2 . 2
5 cbvral.3 . 2
61, 2, 3, 4, 5cbvralf 2653 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104  wnf 1437  wral 2418 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-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1732  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ral 2423 This theorem is referenced by:  cbvralv  2659  cbvralsv  2673  cbviin  3861  frind  4285  ralxpf  4697  eqfnfv2f  5534  ralrnmpt  5574  dff13f  5683  ofrfval2  6010  fmpox  6110  cbvixp  6621  mptelixpg  6640  xpf1o  6750  indstr  9444  fsum3  11217  fsum00  11292  mertenslem2  11366  ctiunctal  12026  cnmpt11  12527  cnmpt21  12535  bj-bdfindes  13363  bj-findes  13395
 Copyright terms: Public domain W3C validator