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

Theorem relopabi 4491
Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
Hypothesis
Ref Expression
relopabi.1  |-  A  =  { <. x ,  y
>.  |  ph }
Assertion
Ref Expression
relopabi  |-  Rel  A

Proof of Theorem relopabi
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 relopabi.1 . . . 4  |-  A  =  { <. x ,  y
>.  |  ph }
2 df-opab 3847 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2076 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2577 . . . . . . . 8  |-  x  e. 
_V
5 vex 2577 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4418 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2116 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( z  e.  ( _V  X.  _V ) 
<-> 
<. x ,  y >.  e.  ( _V  X.  _V ) ) )
86, 7mpbiri 161 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  z  e.  ( _V  X.  _V )
)
98adantr 265 . . . . 5  |-  ( ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
109exlimivv 1792 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3043 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 3003 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4380 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
1412, 13mpbir 138 1  |-  Rel  A
Colors of variables: wff set class
Syntax hints:    /\ wa 101    = wceq 1259   E.wex 1397    e. wcel 1409   {cab 2042   _Vcvv 2574    C_ wss 2945   <.cop 3406   {copab 3845    X. cxp 4371   Rel wrel 4378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-pow 3955  ax-pr 3972
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-opab 3847  df-xp 4379  df-rel 4380
This theorem is referenced by:  relopab  4492  reli  4493  rele  4494  relcnv  4731  cotr  4734  relco  4847  reloprab  5581  reldmoprab  5617  eqer  6169  ecopover  6235  ecopoverg  6238  relen  6256  reldom  6257  enq0er  6591  climrel  10032
  Copyright terms: Public domain W3C validator