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

Theorem cbvex 1925
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 1765 . . . 4  |-  F/ y  -.  ph
3 cbvex.2 . . . . 5  |-  F/ x ps
43nfn 1765 . . . 4  |-  F/ x  -.  ps
5 cbvex.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 285 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 1924 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 287 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1529 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1529 . 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 1527   E.wex 1528   F/wnf 1531
This theorem is referenced by:  cbvexv  1943  cbvex2  1945  exsb  2069  euf  2149  mo  2165  cbvmo  2180  mopick  2205  clelab  2403  issetf  2793  eqvincf  2896  rexab2  2932  euabsn  3699  eluniab  3839  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  axrep1  4132  axrep2  4133  axrep4  4135  opeliunxp  4740  dfdmf  4873  dfrnf  4917  elrnmpt1  4928  opabex3  5769  cbvoprab1  5918  cbvoprab2  5919  zfcndrep  8236  cbvsum  12168  fsum2dlem  12233  elunif  27687  stoweidlem46  27795  bnj1146  28823  bnj607  28948  bnj1228  29041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator