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

Theorem brrelex12 4985
Description: A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
brrelex12  |-  ( ( Rel  R  /\  A R B )  ->  ( A  e.  _V  /\  B  e.  _V ) )

Proof of Theorem brrelex12
StepHypRef Expression
1 df-rel 4956 . . . . 5  |-  ( Rel 
R  <->  R  C_  ( _V 
X.  _V ) )
21biimpi 194 . . . 4  |-  ( Rel 
R  ->  R  C_  ( _V  X.  _V ) )
32ssbrd 4442 . . 3  |-  ( Rel 
R  ->  ( A R B  ->  A ( _V  X.  _V ) B ) )
43imp 429 . 2  |-  ( ( Rel  R  /\  A R B )  ->  A
( _V  X.  _V ) B )
5 brxp 4979 . 2  |-  ( A ( _V  X.  _V ) B  <->  ( A  e. 
_V  /\  B  e.  _V ) )
64, 5sylib 196 1  |-  ( ( Rel  R  /\  A R B )  ->  ( A  e.  _V  /\  B  e.  _V ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   _Vcvv 3078    C_ wss 3437   class class class wbr 4401    X. cxp 4947   Rel wrel 4954
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-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640
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 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-xp 4955  df-rel 4956
This theorem is referenced by:  brrelex  4986  brrelex2  4987  relbrcnvg  5316  ovprc  6228  brovex  6851  ersym  7224  relelec  7252  encv  7429  bren  7430  fsuppunbi  7753  fpwwe2lem2  8911  fpwwelem  8924  fpwwe  8925  isstruct2  14302  brssc  14847  cofuval2  14917  isfull  14940  isfth  14944  isnat  14977  pslem  15496  efgrelexlema  16368  frgpuplem  16391  dvdsr  16862  tpsexOLD  18657  ulmval  21979  iseupa  23739  rngoablo2  24062  opelco3  27734  aovprc  30243  aovrcl  30244  oprabv  30306
  Copyright terms: Public domain W3C validator