Theorem r19.28zv 4450

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ≠ wne 2947  ∀wral 3066  ∅c0 4276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-ne 2948  df-ral 3067  df-dif 3898  df-nul 4277

This theorem is referenced by:  raaanv  4463  raltpd  4730  iinrab  5016  iindif2  5024  iinin2  5025  reusv2lem5  5349  xpiindi  5796  dfpo2  6268  fint  6728  ixpiin  8891  neips  23142  txflf  24035  isclmp  25128  diaglbN  41617  dihglbcpreN  41862  2reuimp  47647