Theorem r19.26 2746

Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

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

Proof of Theorem r19.26

Step	Hyp	Ref	Expression
1		simpl 443	. . . 4 ⊢ ((φ ∧ ψ) → φ)
2	1	ralimi 2689	. . 3 ⊢ (∀x ∈ A (φ ∧ ψ) → ∀x ∈ A φ)
3		simpr 447	. . . 4 ⊢ ((φ ∧ ψ) → ψ)
4	3	ralimi 2689	. . 3 ⊢ (∀x ∈ A (φ ∧ ψ) → ∀x ∈ A ψ)
5	2, 4	jca 518	. 2 ⊢ (∀x ∈ A (φ ∧ ψ) → (∀x ∈ A φ ∧ ∀x ∈ A ψ))
6		pm3.2 434	. . . 4 ⊢ (φ → (ψ → (φ ∧ ψ)))
7	6	ral2imi 2690	. . 3 ⊢ (∀x ∈ A φ → (∀x ∈ A ψ → ∀x ∈ A (φ ∧ ψ)))
8	7	imp 418	. 2 ⊢ ((∀x ∈ A φ ∧ ∀x ∈ A ψ) → ∀x ∈ A (φ ∧ ψ))
9	5, 8	impbii 180	1 ⊢ (∀x ∈ A (φ ∧ ψ) ↔ (∀x ∈ A φ ∧ ∀x ∈ A ψ))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∀wral 2614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2619

This theorem is referenced by:  r19.26-2  2747  r19.26-3  2748  ralbiim  2751  r19.27av  2752  r19.35  2758  reu8  3032  ssrab  3344  r19.28z  3642  r19.28zv  3645  r19.27z  3648  r19.27zv  3649  2ralunsn  3880  iuneq2  3985  fncnv  5158  fnres  5199  fnopabg  5205  eqfnfv3  5394