Theorem bnj121

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

	Ref	Expression
Hypotheses	bnj121.1	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj121.2	No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
	bnj121.3	No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
	bnj121.4	No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
Assertion	bnj121	Could not format assertion : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj121.1	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
2		bnj121.2	Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
3		bnj121.3	Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
4		bnj121.4	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
5	1	sbcbii	$$⊢\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\zeta \leftrightarrow \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
6		bnj105	$$⊢1_{𝑜}\in \mathrm{V}$$
7	6	bnj90	$$⊢\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}fFnn\leftrightarrow fFn{1}_{𝑜}$$
8	7	bicomi	$$⊢fFn{1}_{𝑜}\leftrightarrow \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}fFnn$$
9	8 3 4	3anbi123i	Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> ( [. 1o / n ]. f Fn n /\ [. 1o / n ]. ph /\ [. 1o / n ]. ps ) ) with typecode |-
10		sbc3an	$$⊢\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(fFnn\wedge \phi \wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}fFnn\wedge \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\psi \right)$$
11	9 10	bitr4i	Could not format ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( f Fn 1o /\ ph' /\ ps' ) <-> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) with typecode |-
12	11	imbi2i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> [. 1o / n ]. ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
13		nfv	$$⊢Ⅎn\left(RFrSeA\wedge x\in A\right)$$
14	13	sbc19.21g	$$⊢1_{𝑜}\in \mathrm{V}\to \left(\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(fFnn\wedge \phi \wedge \psi \right)\right)\right)$$
15	6 14	ax-mp	$$⊢\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)\leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
16	12 15	bitr4i	Could not format ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> [. 1o / n ]. ( ( R _FrSe A /\ x e. A ) -> ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
17	5 2 16	3bitr4i	Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-