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

Theorem cbvopabv 4464
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 1674 . 2  |-  F/ z
ph
2 nfv 1674 . 2  |-  F/ w ph
3 nfv 1674 . 2  |-  F/ x ps
4 nfv 1674 . 2  |-  F/ y ps
5 cbvopabv.1 . 2  |-  ( ( x  =  z  /\  y  =  w )  ->  ( ph  <->  ps )
)
61, 2, 3, 4, 5cbvopab 4463 1  |-  { <. x ,  y >.  |  ph }  =  { <. z ,  w >.  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370   {copab 4452
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  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4454
This theorem is referenced by:  cantnf  8007  cantnfOLD  8029  infxpen  8287  axdc2  8724  fpwwe2cbv  8903  fpwwecbv  8917  sylow1  16218  bcth  20967  vitali  21221  lgsquadlem3  22823  lgsquad  22824  axcontlem1  23357  eulerpartlemgvv  26898  eulerpart  26904  cvmlift2lem13  27343  pellex  29319  aomclem8  29557
  Copyright terms: Public domain W3C validator