MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.3rzv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 nfv 1829 . 2 𝑥𝜑
21r19.3rz 4013 1 (𝐴 ≠ ∅ → (𝜑 ↔ ∀𝑥𝐴 𝜑))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator