Theorem r19.28zv 4447

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 4443	1 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ≠ wne 2933  ∀wral 3052  ∅c0 4274

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 2185  ax-ext 2709

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 2716  df-cleq 2729  df-ne 2934  df-ral 3053  df-dif 3893  df-nul 4275

This theorem is referenced by:  raaanv  4460  raltpd  4726  iinrab  5012  iindif2  5020  iinin2  5021  reusv2lem5  5343  xpiindi  5788  dfpo2  6258  fint  6717  ixpiin  8869  neips  23094  txflf  23987  isclmp  25080  diaglbN  41523  dihglbcpreN  41768  2reuimp  47583