Theorem 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	$$⊢\chi \leftrightarrow \left(N\in D\wedge fFnN\wedge \phi \wedge \psi \right)$$
	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 \mathrm{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	$$⊢\chi \leftrightarrow \left(N\in D\wedge fFnN\wedge \phi \wedge \psi \right)$$
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 \mathrm{V}$$
6		sbccow	$$⊢\underset{\dot{}}{[}G/h\underset{\dot{}}{]}\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\chi$$
7		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)$$
8	7	sbcbii	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(N\in D\wedge fFnN\wedge \phi \wedge \psi \right)\leftrightarrow \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(N\in D\wedge \left(fFnN\wedge \phi \wedge \psi \right)\right)$$
9	1	sbcbii	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(N\in D\wedge fFnN\wedge \phi \wedge \psi \right)$$
10		vex	$$⊢h\in \mathrm{V}$$
11	10	bnj525	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}N\in D\leftrightarrow N\in D$$
12		sbc3an	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(fFnN\wedge \phi \wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}fFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
13		bnj62	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}fFnN\leftrightarrow hFnN$$
14	13	3anbi1i	$$⊢\left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}fFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
15	12 14	bitri	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(fFnN\wedge \phi \wedge \psi \right)\leftrightarrow \left(hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
16	11 15	anbi12i	$$⊢\left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}N\in D\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(fFnN\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(N\in D\wedge \left(hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)\right)$$
17		sbcan	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(N\in D\wedge \left(fFnN\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}N\in D\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(fFnN\wedge \phi \wedge \psi \right)\right)$$
18		bnj252	$$⊢\left(N\in D\wedge hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(N\in D\wedge \left(hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)\right)$$
19	16 17 18	3bitr4ri	$$⊢\left(N\in D\wedge hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)\leftrightarrow \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\left(N\in D\wedge \left(fFnN\wedge \phi \wedge \psi \right)\right)$$
20	8 9 19	3bitr4i	$$⊢\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\chi \leftrightarrow \left(N\in D\wedge hFnN\wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
21		fneq1	$$⊢h=G\to \left(hFnN\leftrightarrow GFnN\right)$$
22		sbceq1a	$$⊢h=G\to \left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}G/h\underset{\dot{}}{]}\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \right)$$
23		sbccow	$$⊢\underset{\dot{}}{[}G/h\underset{\dot{}}{]}\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\phi$$
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 \left(\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}G/h\underset{\dot{}}{]}\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
27		sbccow	$$⊢\underset{\dot{}}{[}G/h\underset{\dot{}}{]}\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\psi$$
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	syl5bb	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 |-