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

Theorem cbvex 2023
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 1902 . . . 4  |-  F/ y  -.  ph
3 cbval.2 . . . . 5  |-  F/ x ps
43nfn 1902 . . . 4  |-  F/ x  -.  ps
5 cbval.3 . . . . 5  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
65notbid 294 . . . 4  |-  ( x  =  y  ->  ( -.  ph  <->  -.  ps )
)
72, 4, 6cbval 2022 . . 3  |-  ( A. x  -.  ph  <->  A. y  -.  ps )
87notbii 296 . 2  |-  ( -. 
A. x  -.  ph  <->  -. 
A. y  -.  ps )
9 df-ex 1614 . 2  |-  ( E. x ph  <->  -.  A. x  -.  ph )
10 df-ex 1614 . 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 1393   E.wex 1613   F/wnf 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618
This theorem is referenced by:  cbvexv  2025  cbvex2OLD  2030  sb8e  2169  exsb  2213  euf  2293  mo2  2294  cbvmo  2323  clelab  2601  clelabOLD  2602  issetf  3114  eqvincf  3227  rexab2  3266  euabsn  4104  eluniab  4262  cbvopab1  4527  cbvopab2  4528  cbvopab1s  4529  axrep1  4569  axrep2  4570  axrep4  4572  opeliunxp  5060  dfdmf  5206  dfrnf  5251  elrnmpt1  5261  cbvoprab1  6368  cbvoprab2  6369  opabex3d  6777  opabex3  6778  zfcndrep  9009  fsum2dlem  13596  fprod2dlem  13795  sbcexf  30680  elunif  31552  stoweidlem46  31989  opeliun2xp  33024  bnj1146  33951  bnj607  34075  bnj1228  34168
  Copyright terms: Public domain W3C validator