Theorem r19.26 1289

Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.

Assertion

Ref	Expression
r19.26	⊢ (∀x ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀x ∈ A ψ))

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		jcab 454	. . . 4 ⊢ ((x ∈ A → (φ ∧ ψ)) ↔ ((x ∈ A → φ) ∧ (x ∈ A → ψ)))
2	1	bial 695	. . 3 ⊢ (∀x(x ∈ A → (φ ∧ ψ)) ↔ ∀x((x ∈ A → φ) ∧ (x ∈ A → ψ)))
3		19.26 749	. . 3 ⊢ (∀x((x ∈ A → φ) ∧ (x ∈ A → ψ)) ↔ (∀x(x ∈ A → φ) ∧ ∀x(x ∈ A → ψ)))
4	2, 3	bitr 151	. 2 ⊢ (∀x(x ∈ A → (φ ∧ ψ)) ↔ (∀x(x ∈ A → φ) ∧ ∀x(x ∈ A → ψ)))
5		df-ral 1205	. 2 ⊢ (∀x ∈ A (φ ∧ ψ) ↔ ∀x(x ∈ A → (φ ∧ ψ)))
6		df-ral 1205	. . 3 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
7		df-ral 1205	. . 3 ⊢ (∀x ∈ A ψ ↔ ∀x(x ∈ A → ψ))
8	6, 7	anbi12i 369	. 2 ⊢ ((∀x ∈ A φ ∧ ∀x ∈ A ψ) ↔ (∀x(x ∈ A → φ) ∧ ∀x(x ∈ A → ψ)))
9	4, 5, 8	3bitr4 158	1 ⊢ (∀x ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀x ∈ A ψ))

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

This theorem is referenced by:  r19.26-2 1290  r19.35 1298  r19.28zv 1769  r19.27zv 1771  raaan 1775  iuneq2 2006  fint 2769  tz7.48lem 2993  abianfp 3000  xpmapenlem4 3394  xpmapenlem5 3395  aceq5 3563  ac5b 3574  kmlem6 3585  climunii 4883  infxpidmlem7 4939  hlimunii 5143  ocsh 5164  spanun 5450

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-gen 677

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

metamath.org