Theorem relelfvdm 5704

Description: If a function value has a member, the argument belongs to the domain. (Contributed by Jim Kingdon, 22-Jan-2019.)

Assertion

Ref	Expression
relelfvdm	|- ( ( Rel F /\ A e. ( F ` B ) ) -> B e. dom F )

Proof of Theorem relelfvdm

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfv 5670	. . . . . 6 |- ( A e. ( F ` B ) <-> E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) )
2		exsimpr 1667	. . . . . 6 |- ( E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) -> E. x A. y ( B F y <-> y = x ) )
3	1, 2	sylbi 121	. . . . 5 |- ( A e. ( F ` B ) -> E. x A. y ( B F y <-> y = x ) )
4		equsb1 1834	. . . . . . . 8 |- [ x / y ] y = x
5		spsbbi 1893	. . . . . . . 8 |- ( A. y ( B F y <-> y = x ) -> ( [ x / y ] B F y <-> [ x / y ] y = x ) )
6	4, 5	mpbiri 168	. . . . . . 7 |- ( A. y ( B F y <-> y = x ) -> [ x / y ] B F y )
7		nfv 1577	. . . . . . . 8 |- F/ y B F x
8		breq2 4115	. . . . . . . 8 |- ( y = x -> ( B F y <-> B F x ) )
9	7, 8	sbie 1840	. . . . . . 7 |- ( [ x / y ] B F y <-> B F x )
10	6, 9	sylib 122	. . . . . 6 |- ( A. y ( B F y <-> y = x ) -> B F x )
11	10	eximi 1649	. . . . 5 |- ( E. x A. y ( B F y <-> y = x ) -> E. x B F x )
12	3, 11	syl 14	. . . 4 |- ( A e. ( F ` B ) -> E. x B F x )
13	12	anim2i 342	. . 3 |- ( ( Rel F /\ A e. ( F ` B ) ) -> ( Rel F /\ E. x B F x ) )
14		19.42v 1958	. . 3 |- ( E. x ( Rel F /\ B F x ) <-> ( Rel F /\ E. x B F x ) )
15	13, 14	sylibr 134	. 2 |- ( ( Rel F /\ A e. ( F ` B ) ) -> E. x ( Rel F /\ B F x ) )
16		releldm 4994	. . 3 |- ( ( Rel F /\ B F x ) -> B e. dom F )
17	16	exlimiv 1647	. 2 |- ( E. x ( Rel F /\ B F x ) -> B e. dom F )
18	15, 17	syl 14	1 |- ( ( Rel F /\ A e. ( F ` B ) ) -> B e. dom F )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1396   E.wex 1541   [wsb 1811   e. wcel 2205   class class class wbr 4111   dom cdm 4751   Rel wrel 4756   ` cfv 5354

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 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-xp 4757  df-rel 4758  df-dm 4761  df-iota 5314  df-fv 5362

This theorem is referenced by:  mptrcl  5762  elfvmptrab1  5774  elmpocl  6251  relmptopab  6258  oprssdmm  6367  mpoxopn0yelv  6472  eluzel2  9861  hashinfom  11145  basmex  13289  basmexd  13290  relelbasov  13292  ismgmn0  13588  rrgmex  14423  lssmex  14520  lidlmex  14640  2idlmex  14666  istopon  14895  istps  14914  topontopn  14919  eltg4i  14937  eltg3  14939  tg1  14941  tg2  14942  tgclb  14947  cldrcl  14984  neiss2  15024  lmrcl  15074  cnprcl2k  15088  metflem  15231  xmetf  15232  ismet2  15236  xmeteq0  15241  xmettri2  15243  xmetpsmet  15251  xmetres2  15261  blfvalps  15267  blex  15269  blvalps  15270  blval  15271  blfps  15291  blf  15292  mopnval  15324  isxms2  15334  comet  15381  1vgrex  16032  umgrnloopv  16126