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

Theorem dfoprab2 6352
Description: Class abstraction for operations in terms of class abstraction of ordered pairs. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
dfoprab2  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { <. w ,  z >.  |  E. x E. y ( w  =  <. x ,  y
>.  /\  ph ) }
Distinct variable groups:    x, z, w    y, z, w    ph, w
Allowed substitution hints:    ph( x, y, z)

Proof of Theorem dfoprab2
Dummy variable  v is distinct from all other variables.
StepHypRef Expression
1 excom 1903 . . . 4  |-  ( E. z E. w E. x E. y ( v  =  <. w ,  z
>.  /\  ( w  = 
<. x ,  y >.  /\  ph ) )  <->  E. w E. z E. x E. y ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) ) )
2 exrot4 1908 . . . . 5  |-  ( E. z E. w E. x E. y ( v  =  <. w ,  z
>.  /\  ( w  = 
<. x ,  y >.  /\  ph ) )  <->  E. x E. y E. z E. w ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) ) )
3 opeq1 4187 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  y
>.  ->  <. w ,  z
>.  =  <. <. x ,  y >. ,  z
>. )
43eqeq2d 2436 . . . . . . . . . . 11  |-  ( w  =  <. x ,  y
>.  ->  ( v  = 
<. w ,  z >.  <->  v  =  <. <. x ,  y
>. ,  z >. ) )
54pm5.32ri 642 . . . . . . . . . 10  |-  ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  <->  ( v  = 
<. <. x ,  y
>. ,  z >.  /\  w  =  <. x ,  y >. )
)
65anbi1i 699 . . . . . . . . 9  |-  ( ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )
)
7 anass 653 . . . . . . . . 9  |-  ( ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) ) )
8 an32 805 . . . . . . . . 9  |-  ( ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  ph )  /\  w  =  <. x ,  y >. )
)
96, 7, 83bitr3i 278 . . . . . . . 8  |-  ( ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  ( (
v  =  <. <. x ,  y >. ,  z
>.  /\  ph )  /\  w  =  <. x ,  y >. ) )
109exbii 1712 . . . . . . 7  |-  ( E. w ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) )  <->  E. w
( ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. ) )
11 opex 4685 . . . . . . . . 9  |-  <. x ,  y >.  e.  _V
1211isseti 3086 . . . . . . . 8  |-  E. w  w  =  <. x ,  y >.
13 19.42v 1827 . . . . . . . 8  |-  ( E. w ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. )  <->  ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  E. w  w  =  <. x ,  y >. )
)
1412, 13mpbiran2 927 . . . . . . 7  |-  ( E. w ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. )  <->  ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) )
1510, 14bitri 252 . . . . . 6  |-  ( E. w ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) )  <->  ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph ) )
16153exbii 1714 . . . . 5  |-  ( E. x E. y E. z E. w ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  E. x E. y E. z ( v  =  <. <. x ,  y >. ,  z
>.  /\  ph ) )
172, 16bitri 252 . . . 4  |-  ( E. z E. w E. x E. y ( v  =  <. w ,  z
>.  /\  ( w  = 
<. x ,  y >.  /\  ph ) )  <->  E. x E. y E. z ( v  =  <. <. x ,  y >. ,  z
>.  /\  ph ) )
18 19.42vv 1829 . . . . 5  |-  ( E. x E. y ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  ( v  =  <. w ,  z
>.  /\  E. x E. y ( w  = 
<. x ,  y >.  /\  ph ) ) )
19182exbii 1713 . . . 4  |-  ( E. w E. z E. x E. y ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  E. w E. z ( v  = 
<. w ,  z >.  /\  E. x E. y
( w  =  <. x ,  y >.  /\  ph ) ) )
201, 17, 193bitr3i 278 . . 3  |-  ( E. x E. y E. z ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  <->  E. w E. z ( v  = 
<. w ,  z >.  /\  E. x E. y
( w  =  <. x ,  y >.  /\  ph ) ) )
2120abbii 2551 . 2  |-  { v  |  E. x E. y E. z ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph ) }  =  { v  |  E. w E. z ( v  =  <. w ,  z
>.  /\  E. x E. y ( w  = 
<. x ,  y >.  /\  ph ) ) }
22 df-oprab 6310 . 2  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { v  |  E. x E. y E. z ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
23 df-opab 4483 . 2  |-  { <. w ,  z >.  |  E. x E. y ( w  =  <. x ,  y
>.  /\  ph ) }  =  { v  |  E. w E. z
( v  =  <. w ,  z >.  /\  E. x E. y ( w  =  <. x ,  y
>.  /\  ph ) ) }
2421, 22, 233eqtr4i 2461 1  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { <. w ,  z >.  |  E. x E. y ( w  =  <. x ,  y
>.  /\  ph ) }
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437   E.wex 1657   {cab 2407   <.cop 4004   {copab 4481   {coprab 6307
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-opab 4483  df-oprab 6310
This theorem is referenced by:  reloprab  6353  oprabv  6354  cbvoprab1  6378  cbvoprab12  6380  cbvoprab3  6382  dmoprab  6392  rnoprab  6394  ssoprab2i  6400  mpt2mptx  6402  resoprab  6407  funoprabg  6410  elrnmpt2res  6425  ov6g  6449  dfoprab3s  6863  xpcomco  7672  omxpenlem  7683  nvss  26211  mpt2mptxf  28283  mpt2mptx2  39767
  Copyright terms: Public domain W3C validator