Theorem r19.21v 1713

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

Assertion

Ref	Expression
r19.21v	⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))

Distinct variable group:   φ,x

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		ax-17 969	. . 3 ⊢ (φ → ∀xφ)
2	1	ax-gen 961	. 2 ⊢ ∀x(φ → ∀xφ)
3		r19.21t 1712	. 2 ⊢ (∀x(φ → ∀xφ) → (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ)))
4	2, 3	ax-mp 7	1 ⊢ (∀x ∈ A (φ → ψ) ↔ (φ → ∀x ∈ A ψ))

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952  ∀wral 1642

This theorem is referenced by:  r19.32v 1755  rcla4dv 1874  rmo4 1929  sbcralt 1986  sbcralgf 1988  ssiin 2595  dftr5 2679  tfinds2 3165  tfinds3 3166  tfr3 3928  oeordi 4215  oaabs 4253  raluz2 6395  cau5 6876  climaddlem3 7072  climmullem8 7083  metcn4 7933

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1646

Copyright terms: Public domain