Theorem r19.3rzv 4015

Description: Restricted quantification of wff not containing quantified variable. (Contributed by NM, 10-Mar-1997.)

Assertion

Ref	Expression
r19.3rzv	⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥

Proof of Theorem r19.3rzv

Step	Hyp	Ref	Expression
1		nfv 1829	. 2 ⊢ Ⅎ𝑥𝜑
2	1	r19.3rz 4013	1 ⊢ (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ↔ wb 194   ≠ wne 2779  ∀wral 2895  ∅c0 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-v 3174  df-dif 3542  df-nul 3874

This theorem is referenced by:  r19.9rzv  4016  r19.37zv  4018  iinconst  4460  cnvpo  5575  supicc  12149  coe1mul2lem1  19406  neipeltop  20690  utop3cls  21812  tgcgr4  25171  frgrareg  26437  frgraregord013  26438  poimirlem23  32385  rencldnfi  36186  cvgdvgrat  37317  ralnralall  40091  av-frgraregord013  41530