Theorem relelfvdm 5707

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 5673	. . . . . 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 4118	. . . . . . . 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 4997	. . 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 4114   dom cdm 4754   Rel wrel 4759   ` cfv 5357

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 4233  ax-pow 4292  ax-pr 4327

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 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-xp 4760  df-rel 4761  df-dm 4764  df-iota 5317  df-fv 5365

This theorem is referenced by:  mptrcl  5765  elfvmptrab1  5777  elmpocl  6257  relmptopab  6264  oprssdmm  6378  mpoxopn0yelv  6483  eluzel2  9876  hashinfom  11166  basmex  13356  basmexd  13357  relelbasov  13359  ismgmn0  13621  opprringb  14324  rrgmex  14507  lssmex  14629  lidlmex  14749  2idlmex  14775  istopon  15004  istps  15023  topontopn  15028  eltg4i  15046  eltg3  15048  tg1  15050  tg2  15051  tgclb  15056  cldrcl  15093  neiss2  15133  lmrcl  15183  cnprcl2k  15197  metflem  15340  xmetf  15341  ismet2  15345  xmeteq0  15350  xmettri2  15352  xmetpsmet  15360  xmetres2  15370  blfvalps  15376  blex  15378  blvalps  15379  blval  15380  blfps  15400  blf  15401  mopnval  15433  isxms2  15443  comet  15490  1vgrex  16141  umgrnloopv  16235