Theorem ffnoprval 4091

Description: An operation maps to a class to which all values belong.

Assertion

Ref	Expression
ffnoprval	|- (F:(A X. B)-->C <-> (F Fn (A X. B) /\ A.x e. A A.y e. B (xFy) e. C))

Distinct variable groups:   x,y,A   x,B,y   x,C,y   x,F,y

Proof of Theorem ffnoprval

Step	Hyp	Ref	Expression
1		ffnfv 3904	. 2 |- (F:(A X. B)-->C <-> (F Fn (A X. B) /\ A.w e. (A X. B)(F` w) e. C))
2		fveq2 3800	. . . . . 6 |- (w = <.x, y>. -> (F` w) = (F` <.x, y>.))
3		df-opr 4041	. . . . . 6 |- (xFy) = (F` <.x, y>.)
4	2, 3	syl6eqr 1562	. . . . 5 |- (w = <.x, y>. -> (F` w) = (xFy))
5	4	eleq1d 1577	. . . 4 |- (w = <.x, y>. -> ((F` w) e. C <-> (xFy) e. C))
6	5	ralxp 3275	. . 3 |- (A.w e. (A X. B)(F` w) e. C <-> A.x e. A A.y e. B (xFy) e. C)
7	6	anbi2i 482	. 2 |- ((F Fn (A X. B) /\ A.w e. (A X. B)(F` w) e. C) <-> (F Fn (A X. B) /\ A.x e. A A.y e. B (xFy) e. C))
8	1, 7	bitri 171	1 |- (F:(A X. B)-->C <-> (F Fn (A X. B) /\ A.x e. A A.y e. B (xFy) e. C))

Syntax hints:   <-> wb 144   /\ wa 221   = wceq 988   e. wcel 990  A.wral 1683  <.cop 2456   X. cxp 3223   Fn wfn 3232  -->wf 3233  ` cfv 3237  (class class class)co 4039

This theorem is referenced by:  foprcl 4092  foprval 4095  mapxpen 4584  axaddopr 5354  axmulopr 5355  mulnzcnopr 5788  seq1rn2 6614  seqzrn2 6679  acdc3lem 7611  acdc2lem2 7614  acdc5lem2 7617  acdclem 7619  metxp 7954  issubgi 8241  ghgrpilem4 8255  ringsn 8282

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-fv 3253  df-opr 4041

Copyright terms: Public domain