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

Theorem cbvex 2126
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 1994 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1994 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 300 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 2125 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 302 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1675 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1675 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
118, 9, 103bitr4i 285 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189   A.wal 1453   E.wex 1674   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  cbvexv  2128  sb8e  2265  exsb  2308  euf  2318  mo2  2319  cbvmo  2346  clelab  2587  issetf  3062  eqvincf  3179  rexab2  3217  euabsn  4057  eluniab  4223  cbvopab1  4487  cbvopab2  4488  cbvopab1s  4489  axrep1  4530  axrep2  4531  axrep4  4533  opeliunxp  4905  dfdmf  5047  dfrnf  5092  elrnmpt1  5102  cbvoprab1  6390  cbvoprab2  6391  opabex3d  6798  opabex3  6799  zfcndrep  9065  fsum2dlem  13880  fprod2dlem  14083  bnj1146  29652  bnj607  29776  bnj1228  29869  poimirlem26  32011  sbcexf  32398  elunif  37377  stoweidlem46  37945  opeliun2xp  40387
  Copyright terms: Public domain W3C validator