Theorem relelfvdm 5667

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 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹)

Proof of Theorem relelfvdm

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfv 5633	. . . . . 6 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)))
2		exsimpr 1664	. . . . . 6 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))
3	1, 2	sylbi 121	. . . . 5 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))
4		equsb1 1831	. . . . . . . 8 ⊢ [𝑥 / 𝑦]𝑦 = 𝑥
5		spsbbi 1890	. . . . . . . 8 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ [𝑥 / 𝑦]𝑦 = 𝑥))
6	4, 5	mpbiri 168	. . . . . . 7 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → [𝑥 / 𝑦]𝐵𝐹𝑦)
7		nfv 1574	. . . . . . . 8 ⊢ Ⅎ𝑦 𝐵𝐹𝑥
8		breq2 4090	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥))
9	7, 8	sbie 1837	. . . . . . 7 ⊢ ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥)
10	6, 9	sylib 122	. . . . . 6 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → 𝐵𝐹𝑥)
11	10	eximi 1646	. . . . 5 ⊢ (∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ∃𝑥 𝐵𝐹𝑥)
12	3, 11	syl 14	. . . 4 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥 𝐵𝐹𝑥)
13	12	anim2i 342	. . 3 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
14		19.42v 1953	. . 3 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) ↔ (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
15	13, 14	sylibr 134	. 2 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → ∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥))
16		releldm 4965	. . 3 ⊢ ((Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
17	16	exlimiv 1644	. 2 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
18	15, 17	syl 14	1 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1393  ∃wex 1538  [wsb 1808   ∈ wcel 2200   class class class wbr 4086  dom cdm 4723  Rel wrel 4728  ‘cfv 5324

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-xp 4729  df-rel 4730  df-dm 4733  df-iota 5284  df-fv 5332

This theorem is referenced by:  mptrcl  5725  elfvmptrab1  5737  elmpocl  6212  relmptopab  6219  oprssdmm  6329  mpoxopn0yelv  6400  eluzel2  9750  hashinfom  11030  basmex  13132  basmexd  13133  relelbasov  13135  ismgmn0  13431  rrgmex  14265  lssmex  14359  lidlmex  14479  2idlmex  14505  istopon  14727  istps  14746  topontopn  14751  eltg4i  14769  eltg3  14771  tg1  14773  tg2  14774  tgclb  14779  cldrcl  14816  neiss2  14856  lmrcl  14906  cnprcl2k  14920  metflem  15063  xmetf  15064  ismet2  15068  xmeteq0  15073  xmettri2  15075  xmetpsmet  15083  xmetres2  15093  blfvalps  15099  blex  15101  blvalps  15102  blval  15103  blfps  15123  blf  15124  mopnval  15156  isxms2  15166  comet  15213  1vgrex  15861  umgrnloopv  15955