Theorem relelfvdm 5680

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 5646	. . . . . 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 1833	. . . . . . . 8 |- [ x / y ] y = x
5		spsbbi 1892	. . . . . . . 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 4097	. . . . . . . 8 |- ( y = x -> ( B F y <-> B F x ) )
9	7, 8	sbie 1839	. . . . . . 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 1955	. . 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 4973	. . 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 1810   e. wcel 2202   class class class wbr 4093   dom cdm 4731   Rel wrel 4736   ` cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-xp 4737  df-rel 4738  df-dm 4741  df-iota 5293  df-fv 5341

This theorem is referenced by:  mptrcl  5738  elfvmptrab1  5750  elmpocl  6227  relmptopab  6234  oprssdmm  6343  mpoxopn0yelv  6448  eluzel2  9805  hashinfom  11086  basmex  13205  basmexd  13206  relelbasov  13208  ismgmn0  13504  rrgmex  14339  lssmex  14434  lidlmex  14554  2idlmex  14580  istopon  14807  istps  14826  topontopn  14831  eltg4i  14849  eltg3  14851  tg1  14853  tg2  14854  tgclb  14859  cldrcl  14896  neiss2  14936  lmrcl  14986  cnprcl2k  15000  metflem  15143  xmetf  15144  ismet2  15148  xmeteq0  15153  xmettri2  15155  xmetpsmet  15163  xmetres2  15173  blfvalps  15179  blex  15181  blvalps  15182  blval  15183  blfps  15203  blf  15204  mopnval  15236  isxms2  15246  comet  15293  1vgrex  15944  umgrnloopv  16038