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

Theorem cbvex 1981
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 1839 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1839 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 294 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 1980 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 296 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1588 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1588 . 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 1368   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  cbvexv  1983  cbvex2OLD  1988  sb8e  2134  exsb  2189  euf  2271  eufOLD  2272  mo2  2273  cbvmo  2305  moOLD  2313  mopickOLDOLD  2349  clelab  2596  clelabOLD  2597  issetf  3077  eqvincf  3188  rexab2  3227  euabsn  4050  eluniab  4205  cbvopab1  4465  cbvopab2  4466  cbvopab1s  4467  axrep1  4507  axrep2  4508  axrep4  4510  opeliunxp  4993  dfdmf  5136  dfrnf  5181  elrnmpt1  5191  cbvoprab1  6262  cbvoprab2  6263  opabex3d  6660  opabex3  6661  zfcndrep  8887  fsum2dlem  13350  fprod2dlem  27630  sbcexf  29064  elunif  29881  stoweidlem46  29984  opeliun2xp  30863  bnj1146  32098  bnj607  32222  bnj1228  32315
  Copyright terms: Public domain W3C validator