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

Theorem 1st2ndbr 7452
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 𝐵𝐴𝐵) → (1st𝐴)𝐵(2nd𝐴))

Proof of Theorem 1st2ndbr
StepHypRef Expression
1 1st2nd 7449 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
2 simpr 473 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴𝐵)
31, 2eqeltrrd 2893 . 2 ((Rel 𝐵𝐴𝐵) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
4 df-br 4852 . 2 ((1st𝐴)𝐵(2nd𝐴) ↔ ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
53, 4sylibr 225 1 ((Rel 𝐵𝐴𝐵) → (1st𝐴)𝐵(2nd𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  cop 4383   class class class wbr 4851  Rel wrel 5323  cfv 6104  1st c1st 7399  2nd c2nd 7400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-iota 6067  df-fun 6106  df-fv 6112  df-1st 7401  df-2nd 7402
This theorem is referenced by:  cofuval  16749  cofu1  16751  cofu2  16753  cofucl  16755  cofuass  16756  cofulid  16757  cofurid  16758  funcres  16763  cofull  16801  cofth  16802  isnat2  16815  fuccocl  16831  fucidcl  16832  fuclid  16833  fucrid  16834  fucass  16835  fucsect  16839  fucinv  16840  invfuc  16841  fuciso  16842  natpropd  16843  fucpropd  16844  homahom  16896  homadm  16897  homacd  16898  homadmcd  16899  catciso  16964  prfval  17047  prfcl  17051  prf1st  17052  prf2nd  17053  1st2ndprf  17054  evlfcllem  17069  evlfcl  17070  curf1cl  17076  curf2cl  17079  curfcl  17080  uncf1  17084  uncf2  17085  curfuncf  17086  uncfcurf  17087  diag1cl  17090  diag2cl  17094  curf2ndf  17095  yon1cl  17111  oyon1cl  17119  yonedalem1  17120  yonedalem21  17121  yonedalem3a  17122  yonedalem4c  17125  yonedalem22  17126  yonedalem3b  17127  yonedalem3  17128  yonedainv  17129  yonffthlem  17130  yoniso  17133  utop2nei  22271  utop3cls  22272
  Copyright terms: Public domain W3C validator