Metamath Proof Explorer


Theorem orrabdioph

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

Ref Expression
Assertion orrabdioph t01N|φDiophNt01N|ψDiophNt01N|φψDiophN

Proof

Step Hyp Ref Expression
1 unrab t01N|φt01N|ψ=t01N|φψ
2 diophun t01N|φDiophNt01N|ψDiophNt01N|φt01N|ψDiophN
3 1 2 eqeltrrid t01N|φDiophNt01N|ψDiophNt01N|φψDiophN