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 χ n D F Fn n φ ψ
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 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 χ n D F Fn n φ ψ
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 V
6 1 sbcbii [˙P / n]˙ χ [˙P / n]˙ n D F Fn n φ ψ
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 P D
9 nfv n F Fn P
10 nfsbc1v n [˙P / n]˙ φ
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 n [˙P / n]˙ ψ
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 n D P D
18 fneq2 n = P F Fn n F Fn P
19 sbceq1a n = P φ [˙P / n]˙ φ
20 19 2 bitr4di Could not format ( n = P -> ( ph <-> ph' ) ) : No typesetting found for |- ( n = P -> ( ph <-> ph' ) ) with typecode |-
21 sbceq1a n = P ψ [˙P / n]˙ ψ
22 21 3 bitr4di 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 n D F Fn n φ ψ n D F Fn n φ ψ
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 |-