Theorem r19.28zv 4436

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ≠ wne 2930  ∀wral 3049  ∅c0 4263

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 2184  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 2931  df-ral 3050  df-dif 3888  df-nul 4264

This theorem is referenced by:  raaanv  4449  raltpd  4715  iinrab  5000  iindif2  5008  iinin2  5009  reusv2lem5  5333  xpiindi  5779  dfpo2  6249  fint  6708  ixpiin  8861  neips  23066  txflf  23959  isclmp  25052  diaglbN  41489  dihglbcpreN  41734  2reuimp  47551