# Metamath Proof Explorer

## Theorem bnj919

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

Ref Expression
Hypotheses bnj919.1 ${⊢}{\chi }↔\left({n}\in {D}\wedge {F}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
bnj919.2 No typesetting found for |- ( ph' <-> [. P / n ]. ph ) with typecode |-
bnj919.3 No typesetting found for |- ( ps' <-> [. P / n ]. ps ) with typecode |-
bnj919.4 No typesetting found for |- ( ch' <-> [. P / n ]. ch ) with typecode |-
bnj919.5 ${⊢}{P}\in \mathrm{V}$
Assertion bnj919 Could not format assertion : No typesetting found for |- ( ch' <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 bnj919.1 ${⊢}{\chi }↔\left({n}\in {D}\wedge {F}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
2 bnj919.2 Could not format ( ph' <-> [. P / n ]. ph ) : No typesetting found for |- ( ph' <-> [. P / n ]. ph ) with typecode |-
3 bnj919.3 Could not format ( ps' <-> [. P / n ]. ps ) : No typesetting found for |- ( ps' <-> [. P / n ]. ps ) with typecode |-
4 bnj919.4 Could not format ( ch' <-> [. P / n ]. ch ) : No typesetting found for |- ( ch' <-> [. P / n ]. ch ) with typecode |-
5 bnj919.5 ${⊢}{P}\in \mathrm{V}$
6 1 sbcbii
7 df-bnj17 Could not format ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' ) ) : No typesetting found for |- ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' ) ) with typecode |-
8 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{P}\in {D}$
9 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{F}Fn{P}$
10 nfsbc1v
11 2 10 nfxfr Could not format F/ n ph' : No typesetting found for |- F/ n ph' with typecode |-
12 8 9 11 nf3an Could not format F/ n ( P e. D /\ F Fn P /\ ph' ) : No typesetting found for |- F/ n ( P e. D /\ F Fn P /\ ph' ) with typecode |-
13 nfsbc1v
14 3 13 nfxfr Could not format F/ n ps' : No typesetting found for |- F/ n ps' with typecode |-
15 12 14 nfan Could not format F/ n ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' ) : No typesetting found for |- F/ n ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' ) with typecode |-
16 7 15 nfxfr Could not format F/ n ( P e. D /\ F Fn P /\ ph' /\ ps' ) : No typesetting found for |- F/ n ( P e. D /\ F Fn P /\ ph' /\ ps' ) with typecode |-
17 eleq1 ${⊢}{n}={P}\to \left({n}\in {D}↔{P}\in {D}\right)$
18 fneq2 ${⊢}{n}={P}\to \left({F}Fn{n}↔{F}Fn{P}\right)$
19 sbceq1a
20 19 2 syl6bbr Could not format ( n = P -> ( ph <-> ph' ) ) : No typesetting found for |- ( n = P -> ( ph <-> ph' ) ) with typecode |-
21 sbceq1a
22 21 3 syl6bbr Could not format ( n = P -> ( ps <-> ps' ) ) : No typesetting found for |- ( n = P -> ( ps <-> ps' ) ) with typecode |-
23 18 20 22 3anbi123d Could not format ( n = P -> ( ( F Fn n /\ ph /\ ps ) <-> ( F Fn P /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( n = P -> ( ( F Fn n /\ ph /\ ps ) <-> ( F Fn P /\ ph' /\ ps' ) ) ) with typecode |-
24 17 23 anbi12d Could not format ( n = P -> ( ( n e. D /\ ( F Fn n /\ ph /\ ps ) ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) ) ) : No typesetting found for |- ( n = P -> ( ( n e. D /\ ( F Fn n /\ ph /\ ps ) ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) ) ) with typecode |-
25 bnj252 ${⊢}\left({n}\in {D}\wedge {F}Fn{n}\wedge {\phi }\wedge {\psi }\right)↔\left({n}\in {D}\wedge \left({F}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right)$
26 bnj252 Could not format ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) ) with typecode |-
27 24 25 26 3bitr4g Could not format ( n = P -> ( ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( n = P -> ( ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) ) with typecode |-
28 16 27 sbciegf Could not format ( P e. _V -> ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( P e. _V -> ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) ) with typecode |-
29 5 28 ax-mp Could not format ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) : No typesetting found for |- ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) with typecode |-
30 4 6 29 3bitri Could not format ( ch' <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) with typecode |-