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∀yx∈A∧y∈B→φ↔∀x∀yy∈B∧x∈A→φ
3 alcom ⊢∀x∀yy∈B∧x∈A→φ↔∀y∀xy∈B∧x∈A→φ
4 2 3 bitri ⊢∀x∀yx∈A∧y∈B→φ↔∀y∀xy∈B∧x∈A→φ
5 r2al ⊢∀x∈A∀y∈Bφ↔∀x∀yx∈A∧y∈B→φ
6 r2al ⊢∀y∈B∀x∈Aφ↔∀y∀xy∈B∧x∈A→φ
7 4 5 6 3bitr4i ⊢∀x∈A∀y∈Bφ↔∀y∈B∀x∈Aφ