MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvex Structured version   Unicode version

Theorem cbvex 2078
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
cbval.1  |-  F/ y
ph
cbval.2  |-  F/ x ps
cbval.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvex  |-  ( E. x ph  <->  E. y ps )

Proof of Theorem cbvex
StepHypRef Expression
1 cbval.1 . . . . 5  |-  F/ y
ph
21nfn 1958 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1958 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 295 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 2077 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 297 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1660 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1660 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
118, 9, 103bitr4i 280 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187   A.wal 1435   E.wex 1659   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by:  cbvexv  2080  sb8e  2220  exsb  2264  euf  2276  mo2  2277  cbvmo  2305  clelab  2573  clelabOLD  2574  issetf  3092  eqvincf  3205  rexab2  3244  euabsn  4075  eluniab  4233  cbvopab1  4496  cbvopab2  4497  cbvopab1s  4498  axrep1  4539  axrep2  4540  axrep4  4542  opeliunxp  4906  dfdmf  5048  dfrnf  5093  elrnmpt1  5103  cbvoprab1  6377  cbvoprab2  6378  opabex3d  6785  opabex3  6786  zfcndrep  9038  fsum2dlem  13809  fprod2dlem  14012  bnj1146  29391  bnj607  29515  bnj1228  29608  poimirlem26  31670  sbcexf  32057  elunif  36977  stoweidlem46  37476  opeliun2xp  38874
  Copyright terms: Public domain W3C validator