Theorem func1st2nd 49799

Description: Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025.)

Hypothesis

Ref	Expression
func1st2nd.1	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))

Assertion

Ref	Expression
func1st2nd	⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

Proof of Theorem func1st2nd

Step	Hyp	Ref	Expression
1		relfunc 17918	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 8038	. 2 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
4	1, 2, 3	sylancr 598	1 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5108  Rel wrel 5666  ‘cfv 6536  (class class class)co 7410  1^st c1st 7983  2^nd c2nd 7984   Func cfunc 17910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  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 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7985  df-2nd 7986  df-func 17914

This theorem is referenced by:  func0g2  49813  idfu1stalem  49823  idfu2nda  49826  cofid1a  49835  cofid2a  49836  cofidvala  49839  cofidf2a  49840  cofidf1a  49841  oppfoppc2  49865  funcoppc4  49867  2oppffunc  49869  cofuoppf  49873  idfth  49881  idsubc  49883  uppropd  49904  uptrlem2  49934  uptra  49938  uptrar  49939  uobeqw  49942  uobeq  49943  uptr2a  49945  natoppfb  49954  diag1f1  50030  diag2f1  50032  fuco11b  50060  fucocolem1  50076  fucocolem2  50077  fucocolem3  50078  fucocolem4  50079  fucoco  50080  fucolid  50084  fucorid  50085  fucorid2  50086  postcofval  50087  postcofcl  50088  precofval  50090  precofval2  50092  precofcl  50093  prcoftposcurfucoa  50107  prcof1  50111  prcof2a  50112  prcof2  50113  prcof22a  50115  prcofdiag1  50116  prcofdiag  50117  fucoppclem  50130  fucoppcid  50131  fucoppcco  50132  oppfdiag1  50137  oppfdiag  50139  isinito2lem  50221  termcfuncval  50255  diag1f1olem  50256  diagffth  50261  funcsn  50264  cofuterm  50268  uobeqterm  50269  isinito4  50270  lanval  50342  ranval  50343  lanup  50364  ranup  50365  lmdpropd  50380  cmdpropd  50381  islmd  50388  iscmd  50389  lmddu  50390  termolmd  50393  lmdran  50394  cmdlan  50395