Theorem reeanv 1825

Description: Rearrange existential quantifiers.

Assertion

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

Distinct variable groups:   φ,y   ψ,x   x,y   y,A   x,B

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		anass 450	. . . . 5 ⊢ (((x ∈ A ⋀ y ∈ B) ⋀ (φ ⋀ ψ)) ↔ (x ∈ A ⋀ (y ∈ B ⋀ (φ ⋀ ψ))))
2		an4 517	. . . . 5 ⊢ (((x ∈ A ⋀ y ∈ B) ⋀ (φ ⋀ ψ)) ↔ ((x ∈ A ⋀ φ) ⋀ (y ∈ B ⋀ ψ)))
3	1, 2	bitr3i 182	. . . 4 ⊢ ((x ∈ A ⋀ (y ∈ B ⋀ (φ ⋀ ψ))) ↔ ((x ∈ A ⋀ φ) ⋀ (y ∈ B ⋀ ψ)))
4	3	2exbii 1093	. . 3 ⊢ (∃x∃y(x ∈ A ⋀ (y ∈ B ⋀ (φ ⋀ ψ))) ↔ ∃x∃y((x ∈ A ⋀ φ) ⋀ (y ∈ B ⋀ ψ)))
5		exdistr 1351	. . 3 ⊢ (∃x∃y(x ∈ A ⋀ (y ∈ B ⋀ (φ ⋀ ψ))) ↔ ∃x(x ∈ A ⋀ ∃y(y ∈ B ⋀ (φ ⋀ ψ))))
6		eeanv 1365	. . 3 ⊢ (∃x∃y((x ∈ A ⋀ φ) ⋀ (y ∈ B ⋀ ψ)) ↔ (∃x(x ∈ A ⋀ φ) ⋀ ∃y(y ∈ B ⋀ ψ)))
7	4, 5, 6	3bitr3i 188	. 2 ⊢ (∃x(x ∈ A ⋀ ∃y(y ∈ B ⋀ (φ ⋀ ψ))) ↔ (∃x(x ∈ A ⋀ φ) ⋀ ∃y(y ∈ B ⋀ ψ)))
8		df-rex 1697	. . . 4 ⊢ (∃y ∈ B (φ ⋀ ψ) ↔ ∃y(y ∈ B ⋀ (φ ⋀ ψ)))
9	8	rexbii 1715	. . 3 ⊢ (∃x ∈ A ∃y ∈ B (φ ⋀ ψ) ↔ ∃x ∈ A ∃y(y ∈ B ⋀ (φ ⋀ ψ)))
10		df-rex 1697	. . 3 ⊢ (∃x ∈ A ∃y(y ∈ B ⋀ (φ ⋀ ψ)) ↔ ∃x(x ∈ A ⋀ ∃y(y ∈ B ⋀ (φ ⋀ ψ))))
11	9, 10	bitri 180	. 2 ⊢ (∃x ∈ A ∃y ∈ B (φ ⋀ ψ) ↔ ∃x(x ∈ A ⋀ ∃y(y ∈ B ⋀ (φ ⋀ ψ))))
12		df-rex 1697	. . 3 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))
13		df-rex 1697	. . 3 ⊢ (∃y ∈ B ψ ↔ ∃y(y ∈ B ⋀ ψ))
14	12, 13	anbi12i 493	. 2 ⊢ ((∃x ∈ A φ ⋀ ∃y ∈ B ψ) ↔ (∃x(x ∈ A ⋀ φ) ⋀ ∃y(y ∈ B ⋀ ψ)))
15	7, 11, 14	3bitr4i 190	1 ⊢ (∃x ∈ A ∃y ∈ B (φ ⋀ ψ) ↔ (∃x ∈ A φ ⋀ ∃y ∈ B ψ))

Syntax hints:   ↔ wb 153   ⋀ wa 230   ∈ wcel 999  ∃wex 1021  ∃wrex 1693

This theorem is referenced by:  tfrlem5 3973  unfi 4614  rankxplim3 4776  kmlem9 4835  cvganz 7014  climunii 7188  climaddlem3 7206  climmullem8 7217  infxpidmlem7 7650  tgcl 7713  opnin 7954  xplm 8060  xpcn 8061  hlimuniii 9191  pjtheui 9318  pjpj0i 9338  superpos 10365  irredi 10405  cdjreui 10443  cdj3i 10452  ghomgrpilem2 10471

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-rex 1697

Copyright terms: Public domain