Theorem func1st2nd 49539

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 17818	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 7984	. 2 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
4	1, 2, 3	sylancr 588	1 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5074  Rel wrel 5625  ‘cfv 6487  (class class class)co 7356  1^st c1st 7929  2^nd c2nd 7930   Func cfunc 17810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-func 17814

This theorem is referenced by:  func0g2  49553  idfu1stalem  49563  idfu2nda  49566  cofid1a  49575  cofid2a  49576  cofidvala  49579  cofidf2a  49580  cofidf1a  49581  oppfoppc2  49605  funcoppc4  49607  2oppffunc  49609  cofuoppf  49613  idfth  49621  idsubc  49623  uppropd  49644  uptrlem2  49674  uptra  49678  uptrar  49679  uobeqw  49682  uobeq  49683  uptr2a  49685  natoppfb  49694  diag1f1  49770  diag2f1  49772  fuco11b  49800  fucocolem1  49816  fucocolem2  49817  fucocolem3  49818  fucocolem4  49819  fucoco  49820  fucolid  49824  fucorid  49825  fucorid2  49826  postcofval  49827  postcofcl  49828  precofval  49830  precofval2  49832  precofcl  49833  prcoftposcurfucoa  49847  prcof1  49851  prcof2a  49852  prcof2  49853  prcof22a  49855  prcofdiag1  49856  prcofdiag  49857  fucoppclem  49870  fucoppcid  49871  fucoppcco  49872  oppfdiag1  49877  oppfdiag  49879  isinito2lem  49961  termcfuncval  49995  diag1f1olem  49996  diagffth  50001  funcsn  50004  cofuterm  50008  uobeqterm  50009  isinito4  50010  lanval  50082  ranval  50083  lanup  50104  ranup  50105  lmdpropd  50120  cmdpropd  50121  islmd  50128  iscmd  50129  lmddu  50130  termolmd  50133  lmdran  50134  cmdlan  50135