Theorem relelfvdm 5502

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 5468	. . . . . 6 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)))
2		exsimpr 1598	. . . . . 6 ⊢ (∃𝑥(𝐴 ∈ 𝑥 ∧ ∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥)) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))
3	1, 2	sylbi 120	. . . . 5 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥))
4		equsb1 1765	. . . . . . . 8 ⊢ [𝑥 / 𝑦]𝑦 = 𝑥
5		spsbbi 1824	. . . . . . . 8 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ [𝑥 / 𝑦]𝑦 = 𝑥))
6	4, 5	mpbiri 167	. . . . . . 7 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → [𝑥 / 𝑦]𝐵𝐹𝑦)
7		nfv 1508	. . . . . . . 8 ⊢ Ⅎ𝑦 𝐵𝐹𝑥
8		breq2 3971	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥))
9	7, 8	sbie 1771	. . . . . . 7 ⊢ ([𝑥 / 𝑦]𝐵𝐹𝑦 ↔ 𝐵𝐹𝑥)
10	6, 9	sylib 121	. . . . . 6 ⊢ (∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → 𝐵𝐹𝑥)
11	10	eximi 1580	. . . . 5 ⊢ (∃𝑥∀𝑦(𝐵𝐹𝑦 ↔ 𝑦 = 𝑥) → ∃𝑥 𝐵𝐹𝑥)
12	3, 11	syl 14	. . . 4 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ∃𝑥 𝐵𝐹𝑥)
13	12	anim2i 340	. . 3 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
14		19.42v 1886	. . 3 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) ↔ (Rel 𝐹 ∧ ∃𝑥 𝐵𝐹𝑥))
15	13, 14	sylibr 133	. 2 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → ∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥))
16		releldm 4823	. . 3 ⊢ ((Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
17	16	exlimiv 1578	. 2 ⊢ (∃𝑥(Rel 𝐹 ∧ 𝐵𝐹𝑥) → 𝐵 ∈ dom 𝐹)
18	15, 17	syl 14	1 ⊢ ((Rel 𝐹 ∧ 𝐴 ∈ (𝐹‘𝐵)) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1333  ∃wex 1472  [wsb 1742   ∈ wcel 2128   class class class wbr 3967  dom cdm 4588  Rel wrel 4593  ‘cfv 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4084  ax-pow 4137  ax-pr 4171

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-br 3968  df-opab 4028  df-xp 4594  df-rel 4595  df-dm 4598  df-iota 5137  df-fv 5180

This theorem is referenced by:  mptrcl  5552  elfvmptrab1  5564  elmpocl  6020  oprssdmm  6121  mpoxopn0yelv  6188  eluzel2  9449  hashinfom  10663  istopon  12481  istps  12500  topontopn  12505  eltg4i  12525  eltg3  12527  tg1  12529  tg2  12530  tgclb  12535  cldrcl  12572  neiss2  12612  lmrcl  12661  cnprcl2k  12676  metflem  12819  xmetf  12820  ismet2  12824  xmeteq0  12829  xmettri2  12831  xmetpsmet  12839  xmetres2  12849  blfvalps  12855  blex  12857  blvalps  12858  blval  12859  blfps  12879  blf  12880  mopnval  12912  isxms2  12922  comet  12969