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

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

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . . . 5  |-  F/ y
ph
21nfn 1777 . . . 4  |-  F/ y  -.  ph
3 cbvex.2 . . . . 5  |-  F/ x ps
43nfn 1777 . . . 4  |-  F/ x  -.  ps
5 cbvex.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 285 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 1937 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 287 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1532 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1532 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
118, 9, 103bitr4i 268 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176   A.wal 1530   E.wex 1531   F/wnf 1534
This theorem is referenced by:  cbvexv  1956  cbvex2  1958  exsb  2082  euf  2162  mo  2178  cbvmo  2193  mopick  2218  clelab  2416  issetf  2806  eqvincf  2909  rexab2  2945  euabsn  3712  eluniab  3855  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  axrep1  4148  axrep2  4149  axrep4  4151  opeliunxp  4756  dfdmf  4889  dfrnf  4933  elrnmpt1  4944  opabex3  5785  cbvoprab1  5934  cbvoprab2  5935  zfcndrep  8252  cbvsum  12184  fsum2dlem  12249  elunif  27790  stoweidlem46  27898  opabex3d  28190  bnj1146  29139  bnj607  29264  bnj1228  29357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator