Theorem r19.28zv 4458

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ≠ wne 2931  ∀wral 3050  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-12 2183  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-cleq 2727  df-ne 2932  df-ral 3051  df-dif 3903  df-nul 4285

This theorem is referenced by:  raaanv  4471  raltpd  4737  iinrab  5023  iindif2  5031  iinin2  5032  reusv2lem5  5346  xpiindi  5783  dfpo2  6253  fint  6712  ixpiin  8864  neips  23059  txflf  23952  isclmp  25055  diaglbN  41350  dihglbcpreN  41595  2reuimp  47398