Metamath Proof Explorer


Theorem ralun

Description: Restricted quantification over union. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion ralun xAφxBφxABφ

Proof

Step Hyp Ref Expression
1 ralunb xABφxAφxBφ
2 1 biimpri xAφxBφxABφ