Theorem r2al 1231

Description: Double restricted universal quantification.

Assertion

Ref	Expression
r2al	⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))

Distinct variable group(s):   x,y   y,A

Proof of Theorem r2al

Step	Hyp	Ref	Expression
1		df-ral 1205	. 2 ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x(x ∈ A → ∀y ∈ B φ))
2		19.21v 942	. . . 4 ⊢ (∀y(x ∈ A → (y ∈ B → φ)) ↔ (x ∈ A → ∀y(y ∈ B → φ)))
3		impexp 276	. . . . 5 ⊢ (((x ∈ A ∧ y ∈ B) → φ) ↔ (x ∈ A → (y ∈ B → φ)))
4	3	bial 695	. . . 4 ⊢ (∀y((x ∈ A ∧ y ∈ B) → φ) ↔ ∀y(x ∈ A → (y ∈ B → φ)))
5		df-ral 1205	. . . . 5 ⊢ (∀y ∈ B φ ↔ ∀y(y ∈ B → φ))
6	5	imbi2i 160	. . . 4 ⊢ ((x ∈ A → ∀y ∈ B φ) ↔ (x ∈ A → ∀y(y ∈ B → φ)))
7	2, 4, 6	3bitr4 158	. . 3 ⊢ (∀y((x ∈ A ∧ y ∈ B) → φ) ↔ (x ∈ A → ∀y ∈ B φ))
8	7	bial 695	. 2 ⊢ (∀x∀y((x ∈ A ∧ y ∈ B) → φ) ↔ ∀x(x ∈ A → ∀y ∈ B φ))
9	1, 8	bitr4 154	1 ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ∧ y ∈ B) → φ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  r3al 1240  ralcom 1312  soss 2140  dfwe2 2187  wereu 2197  weinxp 2467  fununi 2705  f1fv 2916  tz7.48lem 2993  tz7.49 2997  inf3lem6 3469  zornlem4 3606  zornlem6 3608  projlem28 5220

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org