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

Theorem 1st2ndbr 7366
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 7363 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
2 simpr 471 . . 3 ((Rel 𝐵𝐴𝐵) → 𝐴𝐵)
31, 2eqeltrrd 2851 . 2 ((Rel 𝐵𝐴𝐵) → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
4 df-br 4787 . 2 ((1st𝐴)𝐵(2nd𝐴) ↔ ⟨(1st𝐴), (2nd𝐴)⟩ ∈ 𝐵)
53, 4sylibr 224 1 ((Rel 𝐵𝐴𝐵) → (1st𝐴)𝐵(2nd𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  cop 4322   class class class wbr 4786  Rel wrel 5254  cfv 6031  1st c1st 7313  2nd c2nd 7314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fv 6039  df-1st 7315  df-2nd 7316
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  22274  utop3cls  22275
  Copyright terms: Public domain W3C validator