Theorem r19.28zv 4465

Description: Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.)

Assertion

Ref	Expression
r19.28zv	⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem r19.28zv

Step	Hyp	Ref	Expression
1		nfv 1947	. 2 ⊢ Ⅎ𝑥𝜑
2	1	r19.28z 4461	1 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ≠ wne 2957  ∀wral 3078  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-ne 2958  df-ral 3079  df-dif 3905  df-nul 4283

This theorem is used by:  raaanv  4478  raltpd  4745  iinrab  5031  iindif2  5041  iinin2  5042  reusv2lem5  5371  xpiindi  5819  dfpo2  6298  fint  6758  ixpiin  8934  neips  23339  txflf  24233  isclmp  25326  diaglbN  41915  dihglbcpreN  42160  2reuimp  47990