This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj985v

Description: Version of bnj985 with an additional disjoint variable condition, not requiring ax-13 . (Contributed by GG, 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 sb8ef 
 |-  ( 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" )