# Metamath Proof Explorer

## Theorem bnj1385

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1385.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
bnj1385.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
bnj1385.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
bnj1385.4 ${⊢}{x}\in {A}\to \forall {f}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
bnj1385.5 No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
bnj1385.6 ${⊢}{E}=\mathrm{dom}{h}\cap \mathrm{dom}{g}$
bnj1385.7 No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h | E ) = ( g | E ) ) ) with typecode |-
Assertion bnj1385 ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$

### Proof

Step Hyp Ref Expression
1 bnj1385.1 ${⊢}{\phi }↔\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}$
2 bnj1385.2 ${⊢}{D}=\mathrm{dom}{f}\cap \mathrm{dom}{g}$
3 bnj1385.3 ${⊢}{\psi }↔\left({\phi }\wedge \forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
4 bnj1385.4 ${⊢}{x}\in {A}\to \forall {f}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
5 bnj1385.5 Could not format ( ph' <-> A. h e. A Fun h ) : No typesetting found for |- ( ph' <-> A. h e. A Fun h ) with typecode |-
6 bnj1385.6 ${⊢}{E}=\mathrm{dom}{h}\cap \mathrm{dom}{g}$
7 bnj1385.7 Could not format ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h | E ) = ( g | E ) ) ) : No typesetting found for |- ( ps' <-> ( ph' /\ A. h e. A A. g e. A ( h | E ) = ( g | E ) ) ) with typecode |-
8 nfv ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \mathrm{Fun}{f}\right)$
9 4 nfcii ${⊢}\underset{_}{Ⅎ}{f}\phantom{\rule{.4em}{0ex}}{A}$
10 9 nfcri ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{h}\in {A}$
11 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{h}$
12 10 11 nfim ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \mathrm{Fun}{h}\right)$
13 eleq1w ${⊢}{f}={h}\to \left({f}\in {A}↔{h}\in {A}\right)$
14 funeq ${⊢}{f}={h}\to \left(\mathrm{Fun}{f}↔\mathrm{Fun}{h}\right)$
15 13 14 imbi12d ${⊢}{f}={h}\to \left(\left({f}\in {A}\to \mathrm{Fun}{f}\right)↔\left({h}\in {A}\to \mathrm{Fun}{h}\right)\right)$
16 8 12 15 cbvalv1 ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \mathrm{Fun}{f}\right)↔\forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \mathrm{Fun}{h}\right)$
17 df-ral ${⊢}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \mathrm{Fun}{f}\right)$
18 df-ral ${⊢}\forall {h}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{h}↔\forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \mathrm{Fun}{h}\right)$
19 16 17 18 3bitr4i ${⊢}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{f}↔\forall {h}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Fun}{h}$
20 19 1 5 3bitr4i Could not format ( ph <-> ph' ) : No typesetting found for |- ( ph <-> ph' ) with typecode |-
21 nfv ${⊢}Ⅎ{h}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
22 nfv ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}$
23 9 22 nfralw ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}$
24 10 23 nfim ${⊢}Ⅎ{f}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}\right)$
25 dmeq ${⊢}{f}={h}\to \mathrm{dom}{f}=\mathrm{dom}{h}$
26 25 ineq1d ${⊢}{f}={h}\to \mathrm{dom}{f}\cap \mathrm{dom}{g}=\mathrm{dom}{h}\cap \mathrm{dom}{g}$
27 26 2 6 3eqtr4g ${⊢}{f}={h}\to {D}={E}$
28 27 reseq2d ${⊢}{f}={h}\to {{f}↾}_{{D}}={{f}↾}_{{E}}$
29 reseq1 ${⊢}{f}={h}\to {{f}↾}_{{E}}={{h}↾}_{{E}}$
30 28 29 eqtrd ${⊢}{f}={h}\to {{f}↾}_{{D}}={{h}↾}_{{E}}$
31 27 reseq2d ${⊢}{f}={h}\to {{g}↾}_{{D}}={{g}↾}_{{E}}$
32 30 31 eqeq12d ${⊢}{f}={h}\to \left({{f}↾}_{{D}}={{g}↾}_{{D}}↔{{h}↾}_{{E}}={{g}↾}_{{E}}\right)$
33 32 ralbidv ${⊢}{f}={h}\to \left(\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}↔\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}\right)$
34 13 33 imbi12d ${⊢}{f}={h}\to \left(\left({f}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)↔\left({h}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}\right)\right)$
35 21 24 34 cbvalv1 ${⊢}\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)↔\forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}\right)$
36 df-ral ${⊢}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}\right)$
37 df-ral ${⊢}\forall {h}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}↔\forall {h}\phantom{\rule{.4em}{0ex}}\left({h}\in {A}\to \forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}\right)$
38 35 36 37 3bitr4i ${⊢}\forall {f}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{f}↾}_{{D}}={{g}↾}_{{D}}↔\forall {h}\in {A}\phantom{\rule{.4em}{0ex}}\forall {g}\in {A}\phantom{\rule{.4em}{0ex}}{{h}↾}_{{E}}={{g}↾}_{{E}}$
39 20 38 anbi12i Could not format ( ( ph /\ A. f e. A A. g e. A ( f | D ) = ( g | D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h | E ) = ( g | E ) ) ) : No typesetting found for |- ( ( ph /\ A. f e. A A. g e. A ( f | D ) = ( g | D ) ) <-> ( ph' /\ A. h e. A A. g e. A ( h | E ) = ( g | E ) ) ) with typecode |-
40 39 3 7 3bitr4i Could not format ( ps <-> ps' ) : No typesetting found for |- ( ps <-> ps' ) with typecode |-
41 5 6 7 bnj1383 Could not format ( ps' -> Fun U. A ) : No typesetting found for |- ( ps' -> Fun U. A ) with typecode |-
42 40 41 sylbi ${⊢}{\psi }\to \mathrm{Fun}\bigcup {A}$