Theorem r19.28zv 4437

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   ≠ wne 2936  ∀wral 3055  ∅c0 4264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-ne 2937  df-ral 3056  df-dif 3888  df-nul 4265

This theorem is referenced by:  raaanv  4450  raltpd  4716  iinrab  5001  iindif2  5009  iinin2  5010  reusv2lem5  5334  xpiindi  5780  dfpo2  6251  fint  6710  ixpiin  8866  neips  23100  txflf  23993  isclmp  25086  diaglbN  41562  dihglbcpreN  41807  2reuimp  47592