Theorem 1st2ndbr 8053

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 8050	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
2		simpr 490	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2862	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5104	. 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 2145  ⟨cop 4590   class class class wbr 5103  Rel wrel 5656  ‘cfv 6538  1^st c1st 7999  2^nd c2nd 8000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001  df-2nd 8002

This theorem is used by:  cofuval  18057  cofu1  18059  cofu2  18061  cofucl  18063  cofuass  18064  cofulid  18065  cofurid  18066  funcres  18071  cofull  18111  cofth  18112  isnat2  18126  fuccocl  18142  fucidcl  18143  fuclid  18144  fucrid  18145  fucass  18146  fucsect  18150  fucinv  18151  invfuc  18152  fuciso  18153  natpropd  18154  fucpropd  18155  homahom  18214  homadm  18215  homacd  18216  homadmcd  18217  catciso  18286  prfval  18373  prfcl  18377  prf1st  18378  prf2nd  18379  1st2ndprf  18380  evlfcllem  18395  evlfcl  18396  curf1cl  18402  curf2cl  18405  curfcl  18406  uncf1  18410  uncf2  18411  curfuncf  18412  uncfcurf  18413  diag1cl  18416  diag2cl  18420  curf2ndf  18421  yon1cl  18437  oyon1cl  18445  yonedalem1  18446  yonedalem21  18447  yonedalem3a  18448  yonedalem4c  18451  yonedalem22  18452  yonedalem3b  18453  yonedalem3  18454  yonedainv  18455  yonffthlem  18456  yoniso  18459  utop2nei  24569  utop3cls  24570  func1st2nd  50183  oppfval2  50244  idfullsubc  50268  fulloppf  50270  fthoppf  50271  up1st2nd2  50295  uptra  50322  uptrar  50323  uptr2a  50329  diag1  50411  fuco11bALT  50445  precofvalALT  50475  thincciso  50560  thincciso2  50562  eufunclem  50628