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

Theorem cbvex 1983
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-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 1811 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1811 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 286 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 1982 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 288 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1551 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1551 . 2  |-  ( E. y ps  <->  -.  A. y  -.  ps )
118, 9, 103bitr4i 269 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177   A.wal 1549   E.wex 1550   F/wnf 1553
This theorem is referenced by:  cbvexv  1985  cbvex2  1991  sb8e  2169  exsb  2207  euf  2287  mo  2303  cbvmo  2318  mopick  2343  clelab  2556  issetf  2961  eqvincf  3064  rexab2  3101  euabsn  3876  eluniab  4027  cbvopab1  4278  cbvopab2  4279  cbvopab1s  4280  axrep1  4321  axrep2  4322  axrep4  4324  opeliunxp  4929  dfdmf  5064  dfrnf  5108  elrnmpt1  5119  opabex3d  5989  opabex3  5990  cbvoprab1  6144  cbvoprab2  6145  zfcndrep  8489  fsum2dlem  12554  fprod2dlem  25304  elunif  27663  stoweidlem46  27771  bnj1146  29162  bnj607  29287  bnj1228  29380
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator