Metamath Proof Explorer


Theorem ralss

Description: Restricted universal quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion ralss A B x A φ x B x A φ

Proof

Step Hyp Ref Expression
1 ssel A B x A x B
2 1 pm4.71rd A B x A x B x A
3 2 imbi1d A B x A φ x B x A φ
4 impexp x B x A φ x B x A φ
5 3 4 bitrdi A B x A φ x B x A φ
6 5 ralbidv2 A B x A φ x B x A φ