Theorem reeanv 1316

Description: Rearrange existential quantifiers.

Assertion

Ref	Expression
reeanv	⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ))

Distinct variable group(s):   φ,y   ψ,x   x,y   y,A   x,B

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		anass 336	. . . . 5 ⊢ (((x ∈ A ∧ y ∈ B) ∧ (φ ∧ ψ)) ↔ (x ∈ A ∧ (y ∈ B ∧ (φ ∧ ψ))))
2		an4 388	. . . . 5 ⊢ (((x ∈ A ∧ y ∈ B) ∧ (φ ∧ ψ)) ↔ ((x ∈ A ∧ φ) ∧ (y ∈ B ∧ ψ)))
3	1, 2	bitr3 153	. . . 4 ⊢ ((x ∈ A ∧ (y ∈ B ∧ (φ ∧ ψ))) ↔ ((x ∈ A ∧ φ) ∧ (y ∈ B ∧ ψ)))
4	3	bi2ex 734	. . 3 ⊢ (∃x∃y(x ∈ A ∧ (y ∈ B ∧ (φ ∧ ψ))) ↔ ∃x∃y((x ∈ A ∧ φ) ∧ (y ∈ B ∧ ψ)))
5		exdistr 967	. . 3 ⊢ (∃x∃y(x ∈ A ∧ (y ∈ B ∧ (φ ∧ ψ))) ↔ ∃x(x ∈ A ∧ ∃y(y ∈ B ∧ (φ ∧ ψ))))
6		eeanv 980	. . 3 ⊢ (∃x∃y((x ∈ A ∧ φ) ∧ (y ∈ B ∧ ψ)) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃y(y ∈ B ∧ ψ)))
7	4, 5, 6	3bitr3 156	. 2 ⊢ (∃x(x ∈ A ∧ ∃y(y ∈ B ∧ (φ ∧ ψ))) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃y(y ∈ B ∧ ψ)))
8		df-rex 1206	. . . 4 ⊢ (∃y ∈ B (φ ∧ ψ) ↔ ∃y(y ∈ B ∧ (φ ∧ ψ)))
9	8	birex 1224	. . 3 ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ ∃x ∈ A ∃y(y ∈ B ∧ (φ ∧ ψ)))
10		df-rex 1206	. . 3 ⊢ (∃x ∈ A ∃y(y ∈ B ∧ (φ ∧ ψ)) ↔ ∃x(x ∈ A ∧ ∃y(y ∈ B ∧ (φ ∧ ψ))))
11	9, 10	bitr 151	. 2 ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ ∃x(x ∈ A ∧ ∃y(y ∈ B ∧ (φ ∧ ψ))))
12		df-rex 1206	. . 3 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
13		df-rex 1206	. . 3 ⊢ (∃y ∈ B ψ ↔ ∃y(y ∈ B ∧ ψ))
14	12, 13	anbi12i 369	. 2 ⊢ ((∃x ∈ A φ ∧ ∃y ∈ B ψ) ↔ (∃x(x ∈ A ∧ φ) ∧ ∃y(y ∈ B ∧ ψ)))
15	7, 11, 14	3bitr4 158	1 ⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678   ∈ wcel 1092  ∃wrex 1202

This theorem is referenced by:  tfrlem5 2953  unfi 3441  kmlem8 3587  climunii 4883  infxpidmlem7 4939  hlimunii 5143  pjthu 5241  pjthu2 5242  pjpj0 5259

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-7 676  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-rex 1206

metamath.org