Metamath Proof Explorer

Theorem bnj976

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

Ref Expression
Hypotheses bnj976.1 
|- ( ch <-> ( N e. D /\ f Fn N /\ ph /\ ps ) )
bnj976.2 
|- ( ph' <-> [. G / f ]. ph )
bnj976.3 
|- ( ps' <-> [. G / f ]. ps )
bnj976.4 
|- ( ch' <-> [. G / f ]. ch )
bnj976.5 
|- G e. _V
Assertion bnj976 
|- ( ch' <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) )

Proof

Step Hyp Ref Expression
1 bnj976.1 
 |-  ( ch <-> ( N e. D /\ f Fn N /\ ph /\ ps ) )
2 bnj976.2 
 |-  ( ph' <-> [. G / f ]. ph )
3 bnj976.3 
 |-  ( ps' <-> [. G / f ]. ps )
4 bnj976.4 
 |-  ( ch' <-> [. G / f ]. ch )
5 bnj976.5 
 |-  G e. _V
6 sbccow 
 |-  ( [. G / h ]. [. h / f ]. ch <-> [. G / f ]. ch )
7 bnj252 
 |-  ( ( N e. D /\ f Fn N /\ ph /\ ps ) <-> ( N e. D /\ ( f Fn N /\ ph /\ ps ) ) )
8 7 sbcbii 
 |-  ( [. h / f ]. ( N e. D /\ f Fn N /\ ph /\ ps ) <-> [. h / f ]. ( N e. D /\ ( f Fn N /\ ph /\ ps ) ) )
9 1 sbcbii 
 |-  ( [. h / f ]. ch <-> [. h / f ]. ( N e. D /\ f Fn N /\ ph /\ ps ) )
10 vex 
 |-  h e. _V
11 10 bnj525 
 |-  ( [. h / f ]. N e. D <-> N e. D )
12 sbc3an 
 |-  ( [. h / f ]. ( f Fn N /\ ph /\ ps ) <-> ( [. h / f ]. f Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) )
13 bnj62 
 |-  ( [. h / f ]. f Fn N <-> h Fn N )
14 13 3anbi1i 
 |-  ( ( [. h / f ]. f Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) )
15 12 14 bitri 
 |-  ( [. h / f ]. ( f Fn N /\ ph /\ ps ) <-> ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) )
16 11 15 anbi12i 
 |-  ( ( [. h / f ]. N e. D /\ [. h / f ]. ( f Fn N /\ ph /\ ps ) ) <-> ( N e. D /\ ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) ) )
17 sbcan 
 |-  ( [. h / f ]. ( N e. D /\ ( f Fn N /\ ph /\ ps ) ) <-> ( [. h / f ]. N e. D /\ [. h / f ]. ( f Fn N /\ ph /\ ps ) ) )
18 bnj252 
 |-  ( ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( N e. D /\ ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) ) )
19 16 17 18 3bitr4ri 
 |-  ( ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> [. h / f ]. ( N e. D /\ ( f Fn N /\ ph /\ ps ) ) )
20 8 9 19 3bitr4i 
 |-  ( [. h / f ]. ch <-> ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) )
21 fneq1 
 |-  ( h = G -> ( h Fn N <-> G Fn N ) )
22 sbceq1a 
 |-  ( h = G -> ( [. h / f ]. ph <-> [. G / h ]. [. h / f ]. ph ) )
23 sbccow 
 |-  ( [. G / h ]. [. h / f ]. ph <-> [. G / f ]. ph )
24 2 23 bitr4i 
 |-  ( ph' <-> [. G / h ]. [. h / f ]. ph )
25 22 24 bitr4di 
 |-  ( h = G -> ( [. h / f ]. ph <-> ph' ) )
26 sbceq1a 
 |-  ( h = G -> ( [. h / f ]. ps <-> [. G / h ]. [. h / f ]. ps ) )
27 sbccow 
 |-  ( [. G / h ]. [. h / f ]. ps <-> [. G / f ]. ps )
28 3 27 bitr4i 
 |-  ( ps' <-> [. G / h ]. [. h / f ]. ps )
29 26 28 bitr4di 
 |-  ( h = G -> ( [. h / f ]. ps <-> ps' ) )
30 21 25 29 3anbi123d 
 |-  ( h = G -> ( ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( G Fn N /\ ph' /\ ps' ) ) )
31 30 anbi2d 
 |-  ( h = G -> ( ( N e. D /\ ( h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) ) )
32 bnj252 
 |-  ( ( N e. D /\ G Fn N /\ ph' /\ ps' ) <-> ( N e. D /\ ( G Fn N /\ ph' /\ ps' ) ) )
33 31 18 32 3bitr4g 
 |-  ( h = G -> ( ( N e. D /\ h Fn N /\ [. h / f ]. ph /\ [. h / f ]. ps ) <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) )
34 20 33 bitrid 
 |-  ( h = G -> ( [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) ) )
35 5 34 sbcie 
 |-  ( [. G / h ]. [. h / f ]. ch <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) )
36 4 6 35 3bitr2i 
 |-  ( ch' <-> ( N e. D /\ G Fn N /\ ph' /\ ps' ) )