Theorem func1st2nd 49545

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 17829	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 7995	. 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 5086  Rel wrel 5636  ‘cfv 6499  (class class class)co 7367  1^st c1st 7940  2^nd c2nd 7941   Func cfunc 17821

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 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376  ax-un 7689

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fv 6507  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-func 17825

This theorem is referenced by:  func0g2  49559  idfu1stalem  49569  idfu2nda  49572  cofid1a  49581  cofid2a  49582  cofidvala  49585  cofidf2a  49586  cofidf1a  49587  oppfoppc2  49611  funcoppc4  49613  2oppffunc  49615  cofuoppf  49619  idfth  49627  idsubc  49629  uppropd  49650  uptrlem2  49680  uptra  49684  uptrar  49685  uobeqw  49688  uobeq  49689  uptr2a  49691  natoppfb  49700  diag1f1  49776  diag2f1  49778  fuco11b  49806  fucocolem1  49822  fucocolem2  49823  fucocolem3  49824  fucocolem4  49825  fucoco  49826  fucolid  49830  fucorid  49831  fucorid2  49832  postcofval  49833  postcofcl  49834  precofval  49836  precofval2  49838  precofcl  49839  prcoftposcurfucoa  49853  prcof1  49857  prcof2a  49858  prcof2  49859  prcof22a  49861  prcofdiag1  49862  prcofdiag  49863  fucoppclem  49876  fucoppcid  49877  fucoppcco  49878  oppfdiag1  49883  oppfdiag  49885  isinito2lem  49967  termcfuncval  50001  diag1f1olem  50002  diagffth  50007  funcsn  50010  cofuterm  50014  uobeqterm  50015  isinito4  50016  lanval  50088  ranval  50089  lanup  50110  ranup  50111  lmdpropd  50126  cmdpropd  50127  islmd  50134  iscmd  50135  lmddu  50136  termolmd  50139  lmdran  50140  cmdlan  50141