Theorem fnovex 6061

Description: The result of an operation is a set. (Contributed by Jim Kingdon, 15-Jan-2019.)

Assertion

Ref	Expression
fnovex	|- ( ( F Fn ( C X. D ) /\ A e. C /\ B e. D ) -> ( A F B ) e. _V )

Proof of Theorem fnovex

Step	Hyp	Ref	Expression
1		df-ov 6031	. 2 |- ( A F B ) = ( F ` <. A , B >. )
2		opelxp 4761	. . . 4 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
3		funfvex 5665	. . . . 5 |- ( ( Fun F /\ <. A , B >. e. dom F ) -> ( F ` <. A , B >. ) e. _V )
4	3	funfni 5439	. . . 4 |- ( ( F Fn ( C X. D ) /\ <. A , B >. e. ( C X. D ) ) -> ( F ` <. A , B >. ) e. _V )
5	2, 4	sylan2br 288	. . 3 |- ( ( F Fn ( C X. D ) /\ ( A e. C /\ B e. D ) ) -> ( F ` <. A , B >. ) e. _V )
6	5	3impb 1226	. 2 |- ( ( F Fn ( C X. D ) /\ A e. C /\ B e. D ) -> ( F ` <. A , B >. ) e. _V )
7	1, 6	eqeltrid 2318	1 |- ( ( F Fn ( C X. D ) /\ A e. C /\ B e. D ) -> ( A F B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005   e. wcel 2202   _Vcvv 2803   <.cop 3676   X. cxp 4729   Fn wfn 5328   ` cfv 5333  (class class class)co 6028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fn 5336  df-fv 5341  df-ov 6031

This theorem is referenced by:  ovelrn  6181  mapsnen  7029  map1  7030  mapen  7075  mapdom1g  7076  mapxpen  7077  xpmapenlem  7078  fzen  10340  hashfacen  11163  wrdexg  11190  omctfn  13144  topnfn  13407  topnvalg  13414  prdsvallem  13435  prdsval  13436  ismhm  13624  mhmex  13625  rhmex  14252  fnpsr  14763  psrelbas  14776  psrplusgg  14779  psraddcl  14781  psr0cl  14782  psr0lid  14783  psrnegcl  14784  psrlinv  14785  psrgrp  14786  psr1clfi  14789  mplvalcoe  14791  mplbascoe  14792  fnmpl  14794  mplsubgfilemcl  14800  mplplusgg  14804  restbasg  14979  tgrest  14980  restco  14985  lmfval  15004  cnfval  15005  cnpfval  15006  cnpval  15009  txrest  15087  ismet  15155  isxmet  15156  xmetunirn  15169  plyval  15543  2omapen  16716  pw1mapen  16718  gfsumval  16809