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

Theorem 1st2ndbr 6726
Description: Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)
Assertion
Ref Expression
1st2ndbr  |-  ( ( Rel  B  /\  A  e.  B )  ->  ( 1st `  A ) B ( 2nd `  A
) )

Proof of Theorem 1st2ndbr
StepHypRef Expression
1 1st2nd 6723 . . 3  |-  ( ( Rel  B  /\  A  e.  B )  ->  A  =  <. ( 1st `  A
) ,  ( 2nd `  A ) >. )
2 simpr 461 . . 3  |-  ( ( Rel  B  /\  A  e.  B )  ->  A  e.  B )
31, 2eqeltrrd 2540 . 2  |-  ( ( Rel  B  /\  A  e.  B )  ->  <. ( 1st `  A ) ,  ( 2nd `  A
) >.  e.  B )
4 df-br 4394 . 2  |-  ( ( 1st `  A ) B ( 2nd `  A
)  <->  <. ( 1st `  A
) ,  ( 2nd `  A ) >.  e.  B
)
53, 4sylibr 212 1  |-  ( ( Rel  B  /\  A  e.  B )  ->  ( 1st `  A ) B ( 2nd `  A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   <.cop 3984   class class class wbr 4393   Rel wrel 4946   ` cfv 5519   1stc1st 6678   2ndc2nd 6679
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-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475
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-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-iota 5482  df-fun 5521  df-fv 5527  df-1st 6680  df-2nd 6681
This theorem is referenced by:  cofuval  14903  cofu1  14905  cofu2  14907  cofucl  14909  cofuass  14910  cofulid  14911  cofurid  14912  funcres  14917  cofull  14955  cofth  14956  isnat2  14969  fuccocl  14985  fucidcl  14986  fuclid  14987  fucrid  14988  fucass  14989  fucsect  14993  fucinv  14994  invfuc  14995  fuciso  14996  natpropd  14997  fucpropd  14998  homahom  15018  homadm  15019  homacd  15020  homadmcd  15021  catciso  15086  prfval  15120  prfcl  15124  prf1st  15125  prf2nd  15126  1st2ndprf  15127  evlfcllem  15142  evlfcl  15143  curf1cl  15149  curf2cl  15152  curfcl  15153  uncf1  15157  uncf2  15158  curfuncf  15159  uncfcurf  15160  diag1cl  15163  diag2cl  15167  curf2ndf  15168  yon1cl  15184  oyon1cl  15192  yonedalem1  15193  yonedalem21  15194  yonedalem3a  15195  yonedalem4c  15198  yonedalem22  15199  yonedalem3b  15200  yonedalem3  15201  yonedainv  15202  yonffthlem  15203  yoniso  15206  utop2nei  19950  utop3cls  19951
  Copyright terms: Public domain W3C validator