Metamath Proof Explorer

Theorem fvelimad

Description: Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fvelimad.x ⊢Ⅎ_xF
fvelimad.f ⊢φ→FFnA
fvelimad.c ⊢φ→C∈FB
Assertion fvelimad ⊢φ→∃x∈A∩BF⁡x=C

Proof

Step Hyp Ref Expression
1 fvelimad.x ⊢Ⅎ_xF
2 fvelimad.f ⊢φ→FFnA
3 fvelimad.c ⊢φ→C∈FB
4 elimag ⊢C∈FB→C∈FB↔∃y∈ByFC
5 4 ibi ⊢C∈FB→∃y∈ByFC
6 3 5 syl ⊢φ→∃y∈ByFC
7 nfv ⊢Ⅎyφ
8 nfre1 ⊢Ⅎy∃y∈A∩BF⁡y=C
9 vex ⊢y∈V
10 9 a1i ⊢φ∧yFC→y∈V
11 3 adantr ⊢φ∧yFC→C∈FB
12 simpr ⊢φ∧yFC→yFC
13 10 11 12 breldmd ⊢φ∧yFC→y∈dom⁡F
14 2 fndmd ⊢φ→dom⁡F=A
15 14 adantr ⊢φ∧yFC→dom⁡F=A
16 13 15 eleqtrd ⊢φ∧yFC→y∈A
17 16 3adant2 ⊢φ∧y∈B∧yFC→y∈A
18 simp2 ⊢φ∧y∈B∧yFC→y∈B
19 17 18 elind ⊢φ∧y∈B∧yFC→y∈A∩B
20 fnfun ⊢FFnA→Fun⁡F
21 2 20 syl ⊢φ→Fun⁡F
22 21 3ad2ant1 ⊢φ∧y∈B∧yFC→Fun⁡F
23 simp3 ⊢φ∧y∈B∧yFC→yFC
24 funbrfv ⊢Fun⁡F→yFC→F⁡y=C
25 22 23 24 sylc ⊢φ∧y∈B∧yFC→F⁡y=C
26 rspe ⊢y∈A∩B∧F⁡y=C→∃y∈A∩BF⁡y=C
27 19 25 26 syl2anc ⊢φ∧y∈B∧yFC→∃y∈A∩BF⁡y=C
28 27 3exp ⊢φ→y∈B→yFC→∃y∈A∩BF⁡y=C
29 7 8 28 rexlimd ⊢φ→∃y∈ByFC→∃y∈A∩BF⁡y=C
30 6 29 mpd ⊢φ→∃y∈A∩BF⁡y=C
31 nfv ⊢ℲyF⁡x=C
32 nfcv ⊢Ⅎ_xy
33 1 32 nffv ⊢Ⅎ_xF⁡y
34 33 nfeq1 ⊢ℲxF⁡y=C
35 fveqeq2 ⊢x=y→F⁡x=C↔F⁡y=C
36 31 34 35 cbvrexw ⊢∃x∈A∩BF⁡x=C↔∃y∈A∩BF⁡y=C
37 30 36 sylibr ⊢φ→∃x∈A∩BF⁡x=C