Metamath Proof Explorer


Theorem ralcom

Description: Commutation of restricted universal quantifiers. See ralcom2 for a version without disjoint variable condition on x , y . This theorem should be used in place of ralcom2 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion ralcom x A y B φ y B x A φ

Proof

Step Hyp Ref Expression
1 ancomst x A y B φ y B x A φ
2 1 2albii x y x A y B φ x y y B x A φ
3 alcom x y y B x A φ y x y B x A φ
4 2 3 bitri x y x A y B φ y x y B x A φ
5 r2al x A y B φ x y x A y B φ
6 r2al y B x A φ y x y B x A φ
7 4 5 6 3bitr4i x A y B φ y B x A φ