Theorem fvimacnv 5818

Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 5492 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)

Assertion

Ref	Expression
fvimacnv	|- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Proof of Theorem fvimacnv

Step	Hyp	Ref	Expression
1		funfvop 5815	. . . . 5 |- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
2		fvex 5701	. . . . . . 7 |- ( F ` A ) e. _V
3		opelcnvg 5019	. . . . . . 7 |- ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
4	2, 3	mpan 670	. . . . . 6 |- ( A e. dom F -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
5	4	adantl 466	. . . . 5 |- ( ( Fun F /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
6	1, 5	mpbird 232	. . . 4 |- ( ( Fun F /\ A e. dom F ) -> <. ( F ` A ) , A >. e. `' F )
7		elimasng 5195	. . . . . 6 |- ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
8	2, 7	mpan 670	. . . . 5 |- ( A e. dom F -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
9	8	adantl 466	. . . 4 |- ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
10	6, 9	mpbird 232	. . 3 |- ( ( Fun F /\ A e. dom F ) -> A e. ( `' F " { ( F ` A ) } ) )
11	2	snss 3999	. . . . 5 |- ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )
12		imass2 5204	. . . . 5 |- ( { ( F ` A ) } C_ B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
13	11, 12	sylbi 195	. . . 4 |- ( ( F ` A ) e. B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
14	13	sseld 3355	. . 3 |- ( ( F ` A ) e. B -> ( A e. ( `' F " { ( F ` A ) } ) -> A e. ( `' F " B ) ) )
15	10, 14	syl5com 30	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )
16		fvimacnvi 5817	. . . 4 |- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )
17	16	ex 434	. . 3 |- ( Fun F -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
18	17	adantr 465	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
19	15, 18	impbid 191	1 |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1756   _Vcvv 2972   C_ wss 3328   {csn 3877   <.cop 3883   `'ccnv 4839   dom cdm 4840   "cima 4843   Fun wfun 5412   ` cfv 5418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-fv 5426

This theorem is referenced by:  funimass3  5819  elpreima  5823  iinpreima  5833  isr0  19310  rnelfmlem  19525  rnelfm  19526  fmfnfmlem2  19528  fmfnfmlem4  19530  fmfnfm  19531  metustidOLD  20134  metustid  20135  metustsymOLD  20136  metustsym  20137  metustexhalfOLD  20138  metustexhalf  20139  xppreima  25964  dstfrvel  26856  ballotlemrv  26902  grpokerinj  28750  arearect  29591  areaquad  29592  diaintclN  34703  dibintclN  34812  dihintcl  34989