Metamath Proof Explorer

Theorem anrabdioph

Description: Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion anrabdioph 
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 inrab 
 |-  ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } i^i { t e. ( NN0 ^m ( 1 ... N ) ) | ps } ) = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) }
2 diophin 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) -> ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } i^i { t e. ( NN0 ^m ( 1 ... N ) ) | ps } ) e. ( Dioph ` N ) )
3 1 2 eqeltrrid 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. ( Dioph ` N ) )