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

Theorem cbvex 1995
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 1849 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1849 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 294 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 1994 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 296 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1597 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1597 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
118, 9, 103bitr4i 277 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184   A.wal 1377   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  cbvexv  1997  cbvex2OLD  2002  sb8e  2148  exsb  2203  euf  2285  eufOLD  2286  mo2  2287  cbvmo  2319  moOLD  2327  mopickOLDOLD  2363  clelab  2611  clelabOLD  2612  issetf  3118  eqvincf  3231  rexab2  3270  euabsn  4099  eluniab  4256  cbvopab1  4517  cbvopab2  4518  cbvopab1s  4519  axrep1  4559  axrep2  4560  axrep4  4562  opeliunxp  5050  dfdmf  5194  dfrnf  5239  elrnmpt1  5249  cbvoprab1  6351  cbvoprab2  6352  opabex3d  6759  opabex3  6760  zfcndrep  8988  fsum2dlem  13541  fprod2dlem  28684  sbcexf  30119  elunif  30969  stoweidlem46  31346  opeliun2xp  31986  bnj1146  32929  bnj607  33053  bnj1228  33146
  Copyright terms: Public domain W3C validator