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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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 syl5eq
 |-  ( 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 } )