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

Theorem relopabi 4424
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 3815 . . . 4  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
31, 2eqtri 2060 . . 3  |-  A  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
4 vex 2557 . . . . . . . 8  |-  x  e. 
_V
5 vex 2557 . . . . . . . 8  |-  y  e. 
_V
64, 5opelvv 4351 . . . . . . 7  |-  <. x ,  y >.  e.  ( _V  X.  _V )
7 eleq1 2100 . . . . . . 7  |-  ( z  =  <. x ,  y
>.  ->  ( z  e.  ( _V  X.  _V ) 
<-> 
<. x ,  y >.  e.  ( _V  X.  _V ) ) )
86, 7mpbiri 157 . . . . . 6  |-  ( z  =  <. x ,  y
>.  ->  z  e.  ( _V  X.  _V )
)
98adantr 261 . . . . 5  |-  ( ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
109exlimivv 1776 . . . 4  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  ph )  ->  z  e.  ( _V  X.  _V )
)
1110abssi 3012 . . 3  |-  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }  C_  ( _V  X.  _V )
123, 11eqsstri 2972 . 2  |-  A  C_  ( _V  X.  _V )
13 df-rel 4313 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
1412, 13mpbir 134 1  |-  Rel  A
Colors of variables: wff set class
Syntax hints:    /\ wa 97    = wceq 1243   E.wex 1381    e. wcel 1393   {cab 2026   _Vcvv 2554    C_ wss 2914   <.cop 3375   {copab 3813    X. cxp 4304   Rel wrel 4311
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3871  ax-pow 3923  ax-pr 3940
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-opab 3815  df-xp 4312  df-rel 4313
This theorem is referenced by:  relopab  4425  reli  4426  rele  4427  relcnv  4664  cotr  4667  relco  4780  reloprab  5514  reldmoprab  5550  eqer  6097  ecopover  6163  ecopoverg  6166  relen  6184  reldom  6185  enq0er  6476  climrel  9640
  Copyright terms: Public domain W3C validator