Metamath Proof Explorer

Theorem rabrenfdioph

Description: Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion rabrenfdioph 
|- ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) /\ { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. ( Dioph ` A ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | [. ( b o. F ) / a ]. ph } e. ( Dioph ` B ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) /\ b e. ( NN0 ^m ( 1 ... B ) ) ) -> b e. ( NN0 ^m ( 1 ... B ) ) )
2 simplr 
 |-  ( ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) /\ b e. ( NN0 ^m ( 1 ... B ) ) ) -> F : ( 1 ... A ) --> ( 1 ... B ) )
3 ovex 
 |-  ( 1 ... A ) e. _V
4 3 mapco2 
 |-  ( ( b e. ( NN0 ^m ( 1 ... B ) ) /\ F : ( 1 ... A ) --> ( 1 ... B ) ) -> ( b o. F ) e. ( NN0 ^m ( 1 ... A ) ) )
5 1 2 4 syl2anc 
 |-  ( ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) /\ b e. ( NN0 ^m ( 1 ... B ) ) ) -> ( b o. F ) e. ( NN0 ^m ( 1 ... A ) ) )
6 5 biantrurd 
 |-  ( ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) /\ b e. ( NN0 ^m ( 1 ... B ) ) ) -> ( [. ( b o. F ) / a ]. ph <-> ( ( b o. F ) e. ( NN0 ^m ( 1 ... A ) ) /\ [. ( b o. F ) / a ]. ph ) ) )
7 nfcv 
 |-  F/_ a ( NN0 ^m ( 1 ... A ) )
8 7 elrabsf 
 |-  ( ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } <-> ( ( b o. F ) e. ( NN0 ^m ( 1 ... A ) ) /\ [. ( b o. F ) / a ]. ph ) )
9 6 8 bitr4di 
 |-  ( ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) /\ b e. ( NN0 ^m ( 1 ... B ) ) ) -> ( [. ( b o. F ) / a ]. ph <-> ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } ) )
10 9 rabbidva 
 |-  ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | [. ( b o. F ) / a ]. ph } = { b e. ( NN0 ^m ( 1 ... B ) ) | ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } } )
11 10 3adant3 
 |-  ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) /\ { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. ( Dioph ` A ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | [. ( b o. F ) / a ]. ph } = { b e. ( NN0 ^m ( 1 ... B ) ) | ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } } )
12 diophren 
 |-  ( ( { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. ( Dioph ` A ) /\ B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } } e. ( Dioph ` B ) )
13 12 3coml 
 |-  ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) /\ { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. ( Dioph ` A ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | ( b o. F ) e. { a e. ( NN0 ^m ( 1 ... A ) ) | ph } } e. ( Dioph ` B ) )
14 11 13 eqeltrd 
 |-  ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) /\ { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. ( Dioph ` A ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | [. ( b o. F ) / a ]. ph } e. ( Dioph ` B ) )