Theorem 1st2ndbr 8063

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

Step	Hyp	Ref	Expression
1		1st2nd 8060	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
2		simpr 490	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2865	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5107	. 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
5	3, 4	sylibr 237	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ⟨cop 4838   class class class wbr 5106  Rel wrel 5660  ‘cfv 6547  1^st c1st 8009  2^nd c2nd 8010

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6501  df-fun 6549  df-fv 6555  df-1st 8011  df-2nd 8012

This theorem is used by:  cofuval  18072  cofu1  18074  cofu2  18076  cofucl  18078  cofuass  18079  cofulid  18080  cofurid  18081  funcres  18086  cofull  18126  cofth  18127  isnat2  18141  fuccocl  18157  fucidcl  18158  fuclid  18159  fucrid  18160  fucass  18161  fucsect  18165  fucinv  18166  invfuc  18167  fuciso  18168  natpropd  18169  fucpropd  18170  homahom  18229  homadm  18230  homacd  18231  homadmcd  18232  catciso  18301  prfval  18388  prfcl  18392  prf1st  18393  prf2nd  18394  1st2ndprf  18395  evlfcllem  18410  evlfcl  18411  curf1cl  18417  curf2cl  18420  curfcl  18421  uncf1  18425  uncf2  18426  curfuncf  18427  uncfcurf  18428  diag1cl  18431  diag2cl  18435  curf2ndf  18436  yon1cl  18452  oyon1cl  18460  yonedalem1  18461  yonedalem21  18462  yonedalem3a  18463  yonedalem4c  18466  yonedalem22  18467  yonedalem3b  18468  yonedalem3  18469  yonedainv  18470  yonffthlem  18471  yoniso  18474  utop2nei  24584  utop3cls  24585  func1st2nd  50335  oppfval2  50398  idfullsubc  50422  fulloppf  50424  fthoppf  50425  up1st2nd2  50449  uptra  50476  uptrar  50477  uptr2a  50483  diag1  50571  fuco11bALT  50605  precofvalALT  50648  thincciso  50733  thincciso2  50735  eufunclem  50801