Theorem funimass4 5899

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.)

Assertion

Ref	Expression
funimass4	|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )

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

Proof of Theorem funimass4

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3478	. . 3 |- ( ( F " A ) C_ B <-> A. y ( y e. ( F " A ) -> y e. B ) )
2		eqcom 2463	. . . . . . . . . 10 |- ( y = ( F ` x ) <-> ( F ` x ) = y )
3		ssel 3483	. . . . . . . . . . . 12 |- ( A C_ dom F -> ( x e. A -> x e. dom F ) )
4		funbrfvb 5890	. . . . . . . . . . . . 13 |- ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> x F y ) )
5	4	ex 432	. . . . . . . . . . . 12 |- ( Fun F -> ( x e. dom F -> ( ( F ` x ) = y <-> x F y ) ) )
6	3, 5	syl9 71	. . . . . . . . . . 11 |- ( A C_ dom F -> ( Fun F -> ( x e. A -> ( ( F ` x ) = y <-> x F y ) ) ) )
7	6	imp31 430	. . . . . . . . . 10 |- ( ( ( A C_ dom F /\ Fun F ) /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
8	2, 7	syl5bb 257	. . . . . . . . 9 |- ( ( ( A C_ dom F /\ Fun F ) /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
9	8	rexbidva 2962	. . . . . . . 8 |- ( ( A C_ dom F /\ Fun F ) -> ( E. x e. A y = ( F ` x ) <-> E. x e. A x F y ) )
10		vex 3109	. . . . . . . . 9 |- y e. _V
11	10	elima 5330	. . . . . . . 8 |- ( y e. ( F " A ) <-> E. x e. A x F y )
12	9, 11	syl6rbbr 264	. . . . . . 7 |- ( ( A C_ dom F /\ Fun F ) -> ( y e. ( F " A ) <-> E. x e. A y = ( F ` x ) ) )
13	12	imbi1d 315	. . . . . 6 |- ( ( A C_ dom F /\ Fun F ) -> ( ( y e. ( F " A ) -> y e. B ) <-> ( E. x e. A y = ( F ` x ) -> y e. B ) ) )
14		r19.23v 2934	. . . . . 6 |- ( A. x e. A ( y = ( F ` x ) -> y e. B ) <-> ( E. x e. A y = ( F ` x ) -> y e. B ) )
15	13, 14	syl6bbr 263	. . . . 5 |- ( ( A C_ dom F /\ Fun F ) -> ( ( y e. ( F " A ) -> y e. B ) <-> A. x e. A ( y = ( F ` x ) -> y e. B ) ) )
16	15	albidv 1718	. . . 4 |- ( ( A C_ dom F /\ Fun F ) -> ( A. y ( y e. ( F " A ) -> y e. B ) <-> A. y A. x e. A ( y = ( F ` x ) -> y e. B ) ) )
17		ralcom4 3125	. . . . 5 |- ( A. x e. A A. y ( y = ( F ` x ) -> y e. B ) <-> A. y A. x e. A ( y = ( F ` x ) -> y e. B ) )
18		fvex 5858	. . . . . . 7 |- ( F ` x ) e. _V
19		eleq1 2526	. . . . . . 7 |- ( y = ( F ` x ) -> ( y e. B <-> ( F ` x ) e. B ) )
20	18, 19	ceqsalv 3134	. . . . . 6 |- ( A. y ( y = ( F ` x ) -> y e. B ) <-> ( F ` x ) e. B )
21	20	ralbii 2885	. . . . 5 |- ( A. x e. A A. y ( y = ( F ` x ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B )
22	17, 21	bitr3i 251	. . . 4 |- ( A. y A. x e. A ( y = ( F ` x ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B )
23	16, 22	syl6bb 261	. . 3 |- ( ( A C_ dom F /\ Fun F ) -> ( A. y ( y e. ( F " A ) -> y e. B ) <-> A. x e. A ( F ` x ) e. B ) )
24	1, 23	syl5bb 257	. 2 |- ( ( A C_ dom F /\ Fun F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
25	24	ancoms 451	1 |- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   A.wal 1396   = wceq 1398   e. wcel 1823   A.wral 2804   E.wrex 2805   C_ wss 3461   class class class wbr 4439   dom cdm 4988   "cima 4991   Fun wfun 5564   ` cfv 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-fv 5578

This theorem is referenced by:  funimass3  5979  funimass5  5980  funconstss  5981  funimassov  6425  fnwelem  6888  cnfcomlem  8134  cnfcomlemOLD  8142  dfac12lem2  8515  ackbij1b  8610  wunom  9087  phimullem  14393  frmdss2  16230  cntzmhm2  16576  dprd2da  17286  frlmsslsp  18998  1stckgenlem  20220  txcnp  20287  ptcnplem  20288  xkopt  20322  xkoinjcn  20354  tgqtop  20379  uzrest  20564  cnflf2  20670  lmflf  20672  txflf  20673  cnextcn  20733  ghmcnp  20779  ucnima  20950  metcnp  21210  tchcph  21846  ovolficcss  22047  opnmbllem  22176  ellimc2  22447  ellimc3  22449  deg1n0ima  22655  dvloglem  23197  logf1o2  23199  dchrghm  23729  usgrares1  24612  xrofsup  27816  eulerpartlemd  28569  erdszelem2  28900  cvmlift3lem7  29034  mclsax  29193  opnmbllem0  30290  filnetlem4  30439  cnres2  30499  icccncfext  31929