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

Theorem cbvopabv 4219
Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.)
Hypothesis
Ref Expression
cbvopabv.1  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  ps )
)
Assertion
Ref Expression
cbvopabv  |-  { <. x ,  y >.  |  ph }  =  { <. z ,  w >.  |  ps }
Distinct variable groups:    x, y,
z, w    ph, z, w    ps, x, y
Allowed substitution hints:    ph( x, y)    ps( z, w)

Proof of Theorem cbvopabv
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ z
ph
2 nfv 1626 . 2  |-  F/ w ph
3 nfv 1626 . 2  |-  F/ x ps
4 nfv 1626 . 2  |-  F/ y ps
5 cbvopabv.1 . 2  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  ps )
)
61, 2, 3, 4, 5cbvopab 4218 1  |-  { <. x ,  y >.  |  ph }  =  { <. z ,  w >.  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649   {copab 4207
This theorem is referenced by:  cantnf  7583  infxpen  7830  axdc2  8263  fpwwe2cbv  8439  fpwwecbv  8453  sylow1  15165  bcth  19152  vitali  19373  lgsquadlem3  21008  lgsquad  21009  cvmlift2lem13  24782  axcontlem1  25618  pellex  26590  aomclem8  26829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-opab 4209
  Copyright terms: Public domain W3C validator