bnj976

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

	Ref	Expression
Hypotheses	bnj976.1	$⊢ χ \leftrightarrow (N \in D \land f Fn N \land φ \land ψ)$
	bnj976.2	No typesetting found for \|- ( ph' <-> [. G / f ]. ph ) with typecode \|-
	bnj976.3	No typesetting found for \|- ( ps' <-> [. G / f ]. ps ) with typecode \|-
	bnj976.4	No typesetting found for \|- ( ch' <-> [. G / f ]. ch ) with typecode \|-
	bnj976.5	$⊢ G \in V$
Assertion	bnj976	Could not format assertion : No typesetting found for \|- ( ch' <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bnj976.1	$⊢ χ \leftrightarrow (N \in D \land f Fn N \land φ \land ψ)$
2		bnj976.2	Could not format ( ph' <-> [. G / f ]. ph ) : No typesetting found for \|- ( ph' <-> [. G / f ]. ph ) with typecode \|-
3		bnj976.3	Could not format ( ps' <-> [. G / f ]. ps ) : No typesetting found for \|- ( ps' <-> [. G / f ]. ps ) with typecode \|-
4		bnj976.4	Could not format ( ch' <-> [. G / f ]. ch ) : No typesetting found for \|- ( ch' <-> [. G / f ]. ch ) with typecode \|-
5		bnj976.5	$⊢ G \in V$
6		sbccow	$⊢ \underset{˙}{[} G / h \underset{˙}{]} \underset{˙}{[} h / f \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} G / f \underset{˙}{]} χ$
7		bnj252	$⊢ (N \in D \land f Fn N \land φ \land ψ) \leftrightarrow (N \in D \land (f Fn N \land φ \land ψ))$
8	7	sbcbii	$⊢ \underset{˙}{[} h / f \underset{˙}{]} (N \in D \land f Fn N \land φ \land ψ) \leftrightarrow \underset{˙}{[} h / f \underset{˙}{]} (N \in D \land (f Fn N \land φ \land ψ))$
9	1	sbcbii	$⊢ \underset{˙}{[} h / f \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} h / f \underset{˙}{]} (N \in D \land f Fn N \land φ \land ψ)$
10		vex	$⊢ h \in V$
11	10	bnj525	$⊢ \underset{˙}{[} h / f \underset{˙}{]} N \in D \leftrightarrow N \in D$
12		sbc3an	$⊢ \underset{˙}{[} h / f \underset{˙}{]} (f Fn N \land φ \land ψ) \leftrightarrow (\underset{˙}{[} h / f \underset{˙}{]} f Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ)$
13		bnj62	$⊢ \underset{˙}{[} h / f \underset{˙}{]} f Fn N \leftrightarrow h Fn N$
14	13	3anbi1i	$⊢ (\underset{˙}{[} h / f \underset{˙}{]} f Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ) \leftrightarrow (h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ)$
15	12 14	bitri	$⊢ \underset{˙}{[} h / f \underset{˙}{]} (f Fn N \land φ \land ψ) \leftrightarrow (h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ)$
16	11 15	anbi12i	$⊢ (\underset{˙}{[} h / f \underset{˙}{]} N \in D \land \underset{˙}{[} h / f \underset{˙}{]} (f Fn N \land φ \land ψ)) \leftrightarrow (N \in D \land (h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ))$
17		sbcan	$⊢ \underset{˙}{[} h / f \underset{˙}{]} (N \in D \land (f Fn N \land φ \land ψ)) \leftrightarrow (\underset{˙}{[} h / f \underset{˙}{]} N \in D \land \underset{˙}{[} h / f \underset{˙}{]} (f Fn N \land φ \land ψ))$
18		bnj252	$⊢ (N \in D \land h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ) \leftrightarrow (N \in D \land (h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ))$
19	16 17 18	3bitr4ri	$⊢ (N \in D \land h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ) \leftrightarrow \underset{˙}{[} h / f \underset{˙}{]} (N \in D \land (f Fn N \land φ \land ψ))$
20	8 9 19	3bitr4i	$⊢ \underset{˙}{[} h / f \underset{˙}{]} χ \leftrightarrow (N \in D \land h Fn N \land \underset{˙}{[} h / f \underset{˙}{]} φ \land \underset{˙}{[} h / f \underset{˙}{]} ψ)$
21		fneq1	$⊢ h = G \to (h Fn N \leftrightarrow G Fn N)$
22		sbceq1a	$⊢ h = G \to (\underset{˙}{[} h / f \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} G / h \underset{˙}{]} \underset{˙}{[} h / f \underset{˙}{]} φ)$
23		sbccow	$⊢ \underset{˙}{[} G / h \underset{˙}{]} \underset{˙}{[} h / f \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} G / f \underset{˙}{]} φ$
24	2 23	bitr4i	Could not format ( ph' <-> [. G / h ]. [. h / f ]. ph ) : No typesetting found for \|- ( ph' <-> [. G / h ]. [. h / f ]. ph ) with typecode \|-
25	22 24	bitr4di	Could not format ( h = G -> ( [. h / f ]. ph <-> ph' ) ) : No typesetting found for \|- ( h = G -> ( [. h / f ]. ph <-> ph' ) ) with typecode \|-
26		sbceq1a	$⊢ h = G \to (\underset{˙}{[} h / f \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} G / h \underset{˙}{]} \underset{˙}{[} h / f \underset{˙}{]} ψ)$
27		sbccow	$⊢ \underset{˙}{[} G / h \underset{˙}{]} \underset{˙}{[} h / f \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} G / f \underset{˙}{]} ψ$
28	3 27	bitr4i	Could not format ( ps' <-> [. G / h ]. [. h / f ]. ps ) : No typesetting found for \|- ( ps' <-> [. G / h ]. [. h / f ]. ps ) with typecode \|-
29	26 28	bitr4di	Could not format ( h = G -> ( [. h / f ]. ps <-> ps' ) ) : No typesetting found for \|- ( h = G -> ( [. h / f ]. ps <-> ps' ) ) with typecode \|-
30	21 25 29	3anbi123d	Could not format ( h = G -> ( ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( G Fn N /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( h = G -> ( ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( G Fn N /\ ph' /\ ps' ) ) ) with typecode \|-
31	30	anbi2d	Could not format ( h = G -> ( ( N e. D /\ ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) ) ) : No typesetting found for \|- ( h = G -> ( ( N e. D /\ ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) ) ) with typecode \|-
32		bnj252	Could not format ( ( N e. D /\ G Fn N /\ ph' /\ ps' ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( ( N e. D /\ G Fn N /\ ph' /\ ps' ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) ) with typecode \|-
33	31 18 32	3bitr4g	Could not format ( h = G -> ( ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( h = G -> ( ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) ) with typecode \|-
34	20 33	bitrid	Could not format ( h = G -> ( [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( h = G -> ( [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) ) with typecode \|-
35	5 34	sbcie	Could not format ( [. G / h ]. [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) : No typesetting found for \|- ( [. G / h ]. [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) with typecode \|-
36	4 6 35	3bitr2i	Could not format ( ch' <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) : No typesetting found for \|- ( ch' <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) with typecode \|-

Metamath Proof Explorer

Theorem bnj976

Proof