Metamath Proof Explorer

Theorem bnj919

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

Ref Expression
Hypotheses bnj919.1 
|- ( ch <-> ( n e. D /\ F Fn n /\ ph /\ ps ) )
bnj919.2 
|- ( ph' <-> [. P / n ]. ph )
bnj919.3 
|- ( ps' <-> [. P / n ]. ps )
bnj919.4 
|- ( ch' <-> [. P / n ]. ch )
bnj919.5 
|- P e. _V
Assertion bnj919 
|- ( ch' <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) )

Proof

Step Hyp Ref Expression
1 bnj919.1 
 |-  ( ch <-> ( n e. D /\ F Fn n /\ ph /\ ps ) )
2 bnj919.2 
 |-  ( ph' <-> [. P / n ]. ph )
3 bnj919.3 
 |-  ( ps' <-> [. P / n ]. ps )
4 bnj919.4 
 |-  ( ch' <-> [. P / n ]. ch )
5 bnj919.5 
 |-  P e. _V
6 1 sbcbii 
 |-  ( [. P / n ]. ch <-> [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) )
7 df-bnj17 
 |-  ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' ) )
8 nfv 
 |-  F/ n P e. D
9 nfv 
 |-  F/ n F Fn P
10 nfsbc1v 
 |-  F/ n [. P / n ]. ph
11 2 10 nfxfr 
 |-  F/ n ph'
12 8 9 11 nf3an 
 |-  F/ n ( P e. D /\ F Fn P /\ ph' )
13 nfsbc1v 
 |-  F/ n [. P / n ]. ps
14 3 13 nfxfr 
 |-  F/ n ps'
15 12 14 nfan 
 |-  F/ n ( ( P e. D /\ F Fn P /\ ph' ) /\ ps' )
16 7 15 nfxfr 
 |-  F/ n ( P e. D /\ F Fn P /\ ph' /\ ps' )
17 eleq1 
 |-  ( n = P -> ( n e. D <-> P e. D ) )
18 fneq2 
 |-  ( n = P -> ( F Fn n <-> F Fn P ) )
19 sbceq1a 
 |-  ( n = P -> ( ph <-> [. P / n ]. ph ) )
20 19 2 bitr4di 
 |-  ( n = P -> ( ph <-> ph' ) )
21 sbceq1a 
 |-  ( n = P -> ( ps <-> [. P / n ]. ps ) )
22 21 3 bitr4di 
 |-  ( n = P -> ( ps <-> ps' ) )
23 18 20 22 3anbi123d 
 |-  ( n = P -> ( ( F Fn n /\ ph /\ ps ) <-> ( F Fn P /\ ph' /\ ps' ) ) )
24 17 23 anbi12d 
 |-  ( n = P -> ( ( n e. D /\ ( F Fn n /\ ph /\ ps ) ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) ) )
25 bnj252 
 |-  ( ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( n e. D /\ ( F Fn n /\ ph /\ ps ) ) )
26 bnj252 
 |-  ( ( P e. D /\ F Fn P /\ ph' /\ ps' ) <-> ( P e. D /\ ( F Fn P /\ ph' /\ ps' ) ) )
27 24 25 26 3bitr4g 
 |-  ( n = P -> ( ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) )
28 16 27 sbciegf 
 |-  ( P e. _V -> ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) ) )
29 5 28 ax-mp 
 |-  ( [. P / n ]. ( n e. D /\ F Fn n /\ ph /\ ps ) <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) )
30 4 6 29 3bitri 
 |-  ( ch' <-> ( P e. D /\ F Fn P /\ ph' /\ ps' ) )