Metamath Proof Explorer

Theorem csboprabg

Description: Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csboprabg 
|- ( A e. V -> [_ A / x ]_ { <. <. y , z >. , d >. | ph } = { <. <. y , z >. , d >. | [. A / x ]. ph } )

Proof

Step Hyp Ref Expression
1 csbab 
 |-  [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) }
2 sbcex2 
 |-  ( [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) )
3 sbcex2 
 |-  ( [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) )
4 sbcex2 
 |-  ( [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) )
5 sbcan 
 |-  ( [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> ( [. A / x ]. c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) )
6 sbcg 
 |-  ( A e. V -> ( [. A / x ]. c = <. <. y , z >. , d >. <-> c = <. <. y , z >. , d >. ) )
7 6 anbi1d 
 |-  ( A e. V -> ( ( [. A / x ]. c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) <-> ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
8 5 7 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
9 8 exbidv 
 |-  ( A e. V -> ( E. d [. A / x ]. ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
10 4 9 bitrid 
 |-  ( A e. V -> ( [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
11 10 exbidv 
 |-  ( A e. V -> ( E. z [. A / x ]. E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
12 3 11 bitrid 
 |-  ( A e. V -> ( [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
13 12 exbidv 
 |-  ( A e. V -> ( E. y [. A / x ]. E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
14 2 13 bitrid 
 |-  ( A e. V -> ( [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) <-> E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) ) )
15 14 abbidv 
 |-  ( A e. V -> { c | [. A / x ]. E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) } )
16 1 15 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) } )
17 df-oprab 
 |-  { <. <. y , z >. , d >. | ph } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) }
18 17 csbeq2i 
 |-  [_ A / x ]_ { <. <. y , z >. , d >. | ph } = [_ A / x ]_ { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ ph ) }
19 df-oprab 
 |-  { <. <. y , z >. , d >. | [. A / x ]. ph } = { c | E. y E. z E. d ( c = <. <. y , z >. , d >. /\ [. A / x ]. ph ) }
20 16 18 19 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ { <. <. y , z >. , d >. | ph } = { <. <. y , z >. , d >. | [. A / x ]. ph } )