Theorem relelfvdm 5405

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 5371	. . . . . 6 |- ( A e. ( F ` B ) <-> E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) )
2		exsimpr 1578	. . . . . 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 120	. . . . 5 |- ( A e. ( F ` B ) -> E. x A. y ( B F y <-> y = x ) )
4		equsb1 1739	. . . . . . . 8 |- [ x / y ] y = x
5		spsbbi 1796	. . . . . . . 8 |- ( A. y ( B F y <-> y = x ) -> ( [ x / y ] B F y <-> [ x / y ] y = x ) )
6	4, 5	mpbiri 167	. . . . . . 7 |- ( A. y ( B F y <-> y = x ) -> [ x / y ] B F y )
7		nfv 1489	. . . . . . . 8 |- F/ y B F x
8		breq2 3897	. . . . . . . 8 |- ( y = x -> ( B F y <-> B F x ) )
9	7, 8	sbie 1745	. . . . . . 7 |- ( [ x / y ] B F y <-> B F x )
10	6, 9	sylib 121	. . . . . 6 |- ( A. y ( B F y <-> y = x ) -> B F x )
11	10	eximi 1560	. . . . 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 337	. . 3 |- ( ( Rel F /\ A e. ( F ` B ) ) -> ( Rel F /\ E. x B F x ) )
14		19.42v 1858	. . 3 |- ( E. x ( Rel F /\ B F x ) <-> ( Rel F /\ E. x B F x ) )
15	13, 14	sylibr 133	. 2 |- ( ( Rel F /\ A e. ( F ` B ) ) -> E. x ( Rel F /\ B F x ) )
16		releldm 4732	. . 3 |- ( ( Rel F /\ B F x ) -> B e. dom F )
17	16	exlimiv 1558	. 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 103   <-> wb 104   A.wal 1310   E.wex 1449   e. wcel 1461   [wsb 1716   class class class wbr 3893   dom cdm 4497   Rel wrel 4502   ` cfv 5079

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-xp 4503  df-rel 4504  df-dm 4507  df-iota 5044  df-fv 5087

This theorem is referenced by:  mptrcl  5455  elfvmptrab1  5467  elmpocl  5920  oprssdmm  6020  mpoxopn0yelv  6087  eluzel2  9226  hashinfom  10410  istopon  12016  istps  12035  topontopn  12040  eltg4i  12060  eltg3  12062  tg1  12064  tg2  12065  tgclb  12070  cldrcl  12107  neiss2  12147  lmrcl  12196  cnprcl2k  12210  metflem  12331  xmetf  12332  ismet2  12336  xmeteq0  12341  xmettri2  12343  xmetpsmet  12351  xmetres2  12361  blfvalps  12367  blex  12369  blvalps  12370  blval  12371  blfps  12391  blf  12392  mopnval  12424  isxms2  12434  comet  12481