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

Theorem 1st2ndbr 7975
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 7972 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
2 simpr 486 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴𝐵)
31, 2eqeltrrd 2839 . 2 ((Rel 𝐵𝐴𝐵) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
4 df-br 5107 . 2 ((1st𝐴)𝐵(2nd𝐴) ↔ ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
53, 4sylibr 233 1 ((Rel 𝐵𝐴𝐵) → (1st𝐴)𝐵(2nd𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  cop 4593   class class class wbr 5106  Rel wrel 5639  cfv 6497  1st c1st 7920  2nd c2nd 7921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fv 6505  df-1st 7922  df-2nd 7923
This theorem is referenced by:  cofuval  17769  cofu1  17771  cofu2  17773  cofucl  17775  cofuass  17776  cofulid  17777  cofurid  17778  funcres  17783  cofull  17822  cofth  17823  isnat2  17836  fuccocl  17854  fucidcl  17855  fuclid  17856  fucrid  17857  fucass  17858  fucsect  17862  fucinv  17863  invfuc  17864  fuciso  17865  natpropd  17866  fucpropd  17867  homahom  17926  homadm  17927  homacd  17928  homadmcd  17929  catciso  17998  prfval  18088  prfcl  18092  prf1st  18093  prf2nd  18094  1st2ndprf  18095  evlfcllem  18111  evlfcl  18112  curf1cl  18118  curf2cl  18121  curfcl  18122  uncf1  18126  uncf2  18127  curfuncf  18128  uncfcurf  18129  diag1cl  18132  diag2cl  18136  curf2ndf  18137  yon1cl  18153  oyon1cl  18161  yonedalem1  18162  yonedalem21  18163  yonedalem3a  18164  yonedalem4c  18167  yonedalem22  18168  yonedalem3b  18169  yonedalem3  18170  yonedainv  18171  yonffthlem  18172  yoniso  18175  utop2nei  23605  utop3cls  23606  thincciso  47076
  Copyright terms: Public domain W3C validator