Theorem bnj985v

Description: Version of bnj985 with an additional disjoint variable condition, not requiring ax-13 . (Contributed by Gino Giotto, 27-Mar-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj985v.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj985v.6	No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
	bnj985v.9	No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
	bnj985v.11	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
	bnj985v.13	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
Assertion	bnj985v	Could not format assertion : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj985v.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
2		bnj985v.6	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
3		bnj985v.9	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
4		bnj985v.11	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
5		bnj985v.13	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
6	5	bnj918	$$⊢G\in \mathrm{V}$$
7	1 4	bnj984	$$⊢G\in \mathrm{V}\to \left(G\in B\leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\exists n\chi \right)$$
8	6 7	ax-mp	$$⊢G\in B\leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\exists n\chi$$
9		sbcex2	Could not format ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' ) : No typesetting found for |- ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' ) with typecode |-
10		nfv	$$⊢Ⅎp\chi$$
11	10	sb8ev	$$⊢\exists n\chi \leftrightarrow \exists p\left[p/n\right]\chi$$
12		sbsbc	$$⊢\left[p/n\right]\chi \leftrightarrow \underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
13	12	exbii	$$⊢\exists p\left[p/n\right]\chi \leftrightarrow \exists p\underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
14	11 13	bitri	$$⊢\exists n\chi \leftrightarrow \exists p\underset{\dot{}}{[}p/n\underset{\dot{}}{]}\chi$$
15	14 2	bnj133	Could not format ( E. n ch <-> E. p ch' ) : No typesetting found for |- ( E. n ch <-> E. p ch' ) with typecode |-
16	15	sbcbii	Could not format ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' ) : No typesetting found for |- ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' ) with typecode |-
17	3	exbii	Could not format ( E. p ch" <-> E. p [. G / f ]. ch' ) : No typesetting found for |- ( E. p ch" <-> E. p [. G / f ]. ch' ) with typecode |-
18	9 16 17	3bitr4i	Could not format ( [. G / f ]. E. n ch <-> E. p ch" ) : No typesetting found for |- ( [. G / f ]. E. n ch <-> E. p ch" ) with typecode |-
19	8 18	bitri	Could not format ( G e. B <-> E. p ch" ) : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-