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	$⊢ χ \leftrightarrow (n \in D \land F Fn n \land φ \land ψ)$
	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 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	$⊢ χ \leftrightarrow (n \in D \land F Fn n \land φ \land ψ)$
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 V$
6	1	sbcbii	$⊢ \underset{˙}{[} P / n \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} P / n \underset{˙}{]} (n \in D \land F Fn n \land φ \land ψ)$
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 \in D$
9		nfv	$⊢ Ⅎ n F Fn P$
10		nfsbc1v	$⊢ Ⅎ n \underset{˙}{[} P / n \underset{˙}{]} φ$
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{˙}{[} P / n \underset{˙}{]} ψ$
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 (n \in D \leftrightarrow P \in D)$
18		fneq2	$⊢ n = P \to (F Fn n \leftrightarrow F Fn P)$
19		sbceq1a	$⊢ n = P \to (φ \leftrightarrow \underset{˙}{[} P / n \underset{˙}{]} φ)$
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 \to (ψ \leftrightarrow \underset{˙}{[} P / n \underset{˙}{]} ψ)$
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 \in D \land F Fn n \land φ \land ψ) \leftrightarrow (n \in D \land (F Fn n \land φ \land ψ))$
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 \|-

Metamath Proof Explorer

Theorem bnj919

Proof