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 \leftrightarrow \left(n\in D\wedge FFnn\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 \leftrightarrow \left(n\in D\wedge FFnn\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	$$⊢\underset{\dot{}}{[}P/n\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}P/n\underset{\dot{}}{]}\left(n\in D\wedge FFnn\wedge \phi \wedge \psi \right)$$
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	$$⊢ℲnP\in D$$
9		nfv	$$⊢ℲnFFnP$$
10		nfsbc1v	$$⊢Ⅎn\underset{\dot{}}{[}P/n\underset{\dot{}}{]}\phi$$
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\underset{\dot{}}{[}P/n\underset{\dot{}}{]}\psi$$
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\leftrightarrow P\in D\right)$$
18		fneq2	$$⊢n=P\to \left(FFnn\leftrightarrow FFnP\right)$$
19		sbceq1a	$$⊢n=P\to \left(\phi \leftrightarrow \underset{\dot{}}{[}P/n\underset{\dot{}}{]}\phi \right)$$
20	19 2	syl6bbr	Could not format ( n = P -> ( ph <-> ph' ) ) : No typesetting found for |- ( n = P -> ( ph <-> ph' ) ) with typecode |-
21		sbceq1a	$$⊢n=P\to \left(\psi \leftrightarrow \underset{\dot{}}{[}P/n\underset{\dot{}}{]}\psi \right)$$
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 FFnn\wedge \phi \wedge \psi \right)\leftrightarrow \left(n\in D\wedge \left(FFnn\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 |-