ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfoprab2 Unicode version

Theorem dfoprab2 5965
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 1675 . . . 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 1702 . . . . 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 3804 . . . . . . . . . . . 12  |-  ( w  =  <. x ,  y
>.  ->  <. w ,  z
>.  =  <. <. x ,  y >. ,  z
>. )
43eqeq2d 2205 . . . . . . . . . . 11  |-  ( w  =  <. x ,  y
>.  ->  ( v  = 
<. w ,  z >.  <->  v  =  <. <. x ,  y
>. ,  z >. ) )
54pm5.32ri 455 . . . . . . . . . 10  |-  ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  <->  ( v  = 
<. <. x ,  y
>. ,  z >.  /\  w  =  <. x ,  y >. )
)
65anbi1i 458 . . . . . . . . 9  |-  ( ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )
)
7 anass 401 . . . . . . . . 9  |-  ( ( ( v  =  <. w ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) ) )
8 an32 562 . . . . . . . . 9  |-  ( ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  w  =  <. x ,  y
>. )  /\  ph )  <->  ( ( v  =  <. <.
x ,  y >. ,  z >.  /\  ph )  /\  w  =  <. x ,  y >. )
)
96, 7, 83bitr3i 210 . . . . . . . 8  |-  ( ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  ( (
v  =  <. <. x ,  y >. ,  z
>.  /\  ph )  /\  w  =  <. x ,  y >. ) )
109exbii 1616 . . . . . . 7  |-  ( E. w ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) )  <->  E. w
( ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. ) )
11 vex 2763 . . . . . . . . . 10  |-  x  e. 
_V
12 vex 2763 . . . . . . . . . 10  |-  y  e. 
_V
1311, 12opex 4258 . . . . . . . . 9  |-  <. x ,  y >.  e.  _V
1413isseti 2768 . . . . . . . 8  |-  E. w  w  =  <. x ,  y >.
15 19.42v 1918 . . . . . . . 8  |-  ( E. w ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. )  <->  ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  E. w  w  =  <. x ,  y >. )
)
1614, 15mpbiran2 943 . . . . . . 7  |-  ( E. w ( ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph )  /\  w  =  <. x ,  y
>. )  <->  ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) )
1710, 16bitri 184 . . . . . 6  |-  ( E. w ( v  = 
<. w ,  z >.  /\  ( w  =  <. x ,  y >.  /\  ph ) )  <->  ( v  =  <. <. x ,  y
>. ,  z >.  /\ 
ph ) )
18173exbii 1618 . . . . 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 ) )
192, 18bitri 184 . . . 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 ) )
20 19.42vv 1923 . . . . 5  |-  ( E. x E. y ( v  =  <. w ,  z >.  /\  (
w  =  <. x ,  y >.  /\  ph ) )  <->  ( v  =  <. w ,  z
>.  /\  E. x E. y ( w  = 
<. x ,  y >.  /\  ph ) ) )
21202exbii 1617 . . . 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 ) ) )
221, 19, 213bitr3i 210 . . 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 ) ) )
2322abbii 2309 . 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 ) ) }
24 df-oprab 5922 . 2  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { v  |  E. x E. y E. z ( v  = 
<. <. x ,  y
>. ,  z >.  /\ 
ph ) }
25 df-opab 4091 . 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 ) ) }
2623, 24, 253eqtr4i 2224 1  |-  { <. <.
x ,  y >. ,  z >.  |  ph }  =  { <. w ,  z >.  |  E. x E. y ( w  =  <. x ,  y
>.  /\  ph ) }
Colors of variables: wff set class
Syntax hints:    /\ wa 104    = wceq 1364   E.wex 1503   {cab 2179   <.cop 3621   {copab 4089   {coprab 5919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-opab 4091  df-oprab 5922
This theorem is referenced by:  reloprab  5966  cbvoprab1  5990  cbvoprab12  5992  cbvoprab3  5994  dmoprab  5999  rnoprab  6001  ssoprab2i  6007  mpomptx  6009  resoprab  6014  funoprabg  6017  ov6g  6056  dfoprab3s  6243  xpcomco  6880
  Copyright terms: Public domain W3C validator