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	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
	bnj985v.6	|- ( ch' <-> [. p / n ]. ch )
	bnj985v.9	|- ( ch" <-> [. G / f ]. ch' )
	bnj985v.11	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
	bnj985v.13	|- G = ( f u. { <. n , C >. } )
Assertion	bnj985v	|- ( G e. B <-> E. p ch" )

Proof

Step	Hyp	Ref	Expression
1		bnj985v.3	|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2		bnj985v.6	|- ( ch' <-> [. p / n ]. ch )
3		bnj985v.9	|- ( ch" <-> [. G / f ]. ch' )
4		bnj985v.11	|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
5		bnj985v.13	|- G = ( f u. { <. n , C >. } )
6	5	bnj918	|- G e. _V
7	1 4	bnj984	|- ( G e. _V -> ( G e. B <-> [. G / f ]. E. n ch ) )
8	6 7	ax-mp	|- ( G e. B <-> [. G / f ]. E. n ch )
9		sbcex2	|- ( [. G / f ]. E. p ch' <-> E. p [. G / f ]. ch' )
10		nfv	|- F/ p ch
11	10	sb8ev	|- ( E. n ch <-> E. p [ p / n ] ch )
12		sbsbc	|- ( [ p / n ] ch <-> [. p / n ]. ch )
13	12	exbii	|- ( E. p [ p / n ] ch <-> E. p [. p / n ]. ch )
14	11 13	bitri	|- ( E. n ch <-> E. p [. p / n ]. ch )
15	14 2	bnj133	|- ( E. n ch <-> E. p ch' )
16	15	sbcbii	|- ( [. G / f ]. E. n ch <-> [. G / f ]. E. p ch' )
17	3	exbii	|- ( E. p ch" <-> E. p [. G / f ]. ch' )
18	9 16 17	3bitr4i	|- ( [. G / f ]. E. n ch <-> E. p ch" )
19	8 18	bitri	|- ( G e. B <-> E. p ch" )