Theorem fvimacnv 6025

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 5683 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 6022	. . . . 5 |- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
2		fvex 5902	. . . . . . 7 |- ( F ` A ) e. _V
3		opelcnvg 5036	. . . . . . 7 |- ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
4	2, 3	mpan 681	. . . . . 6 |- ( A e. dom F -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
5	4	adantl 472	. . . . 5 |- ( ( Fun F /\ A e. dom F ) -> ( <. ( F ` A ) , A >. e. `' F <-> <. A , ( F ` A ) >. e. F ) )
6	1, 5	mpbird 240	. . . 4 |- ( ( Fun F /\ A e. dom F ) -> <. ( F ` A ) , A >. e. `' F )
7		elimasng 5216	. . . . . 6 |- ( ( ( F ` A ) e. _V /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
8	2, 7	mpan 681	. . . . 5 |- ( A e. dom F -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
9	8	adantl 472	. . . 4 |- ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " { ( F ` A ) } ) <-> <. ( F ` A ) , A >. e. `' F ) )
10	6, 9	mpbird 240	. . 3 |- ( ( Fun F /\ A e. dom F ) -> A e. ( `' F " { ( F ` A ) } ) )
11	2	snss 4109	. . . . 5 |- ( ( F ` A ) e. B <-> { ( F ` A ) } C_ B )
12		imass2 5226	. . . . 5 |- ( { ( F ` A ) } C_ B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
13	11, 12	sylbi 200	. . . 4 |- ( ( F ` A ) e. B -> ( `' F " { ( F ` A ) } ) C_ ( `' F " B ) )
14	13	sseld 3443	. . 3 |- ( ( F ` A ) e. B -> ( A e. ( `' F " { ( F ` A ) } ) -> A e. ( `' F " B ) ) )
15	10, 14	syl5com 31	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B -> A e. ( `' F " B ) ) )
16		fvimacnvi 6024	. . . 4 |- ( ( Fun F /\ A e. ( `' F " B ) ) -> ( F ` A ) e. B )
17	16	ex 440	. . 3 |- ( Fun F -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
18	17	adantr 471	. 2 |- ( ( Fun F /\ A e. dom F ) -> ( A e. ( `' F " B ) -> ( F ` A ) e. B ) )
19	15, 18	impbid 195	1 |- ( ( Fun F /\ A e. dom F ) -> ( ( F ` A ) e. B <-> A e. ( `' F " B ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   e. wcel 1898   _Vcvv 3057   C_ wss 3416   {csn 3980   <.cop 3986   `'ccnv 4855   dom cdm 4856   "cima 4859   Fun wfun 5599   ` cfv 5605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-fv 5613

This theorem is referenced by:  funimass3  6026  elpreima  6030  iinpreima  6038  isr0  20807  rnelfmlem  21022  rnelfm  21023  fmfnfmlem2  21025  fmfnfmlem4  21027  fmfnfm  21028  metustid  21624  metustsym  21625  metustexhalf  21626  xppreima  28301  dstfrvel  29356  ballotlemrv  29402  ballotlemrvOLD  29440  grpokerinj  32229  diaintclN  34672  dibintclN  34781  dihintcl  34958  arearect  36146  areaquad  36147