Theorem r19.28zv 4462

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 1936	. 2 ⊢ Ⅎ𝑥𝜑
2	1	r19.28z 4458	1 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ≠ wne 2959  ∀wral 3078  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-cleq 2756  df-ne 2960  df-ral 3079  df-dif 3909  df-nul 4288

This theorem is referenced by:  raaanv  4475  raltpd  4742  iinrab  5028  iindif2  5036  iinin2  5037  reusv2lem5  5361  xpiindi  5809  dfpo2  6285  fint  6745  ixpiin  8908  neips  23175  txflf  24068  isclmp  25161  diaglbN  41684  dihglbcpreN  41929  2reuimp  47714