MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21v Structured version   Visualization version   GIF version

Theorem 19.21v 2020
Description: Version of 19.21 2231 with a dv condition, requiring fewer axioms.

Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as 𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1858) instead of a dv condition. For instance, 19.21v 2020 versus 19.21 2231 and vtoclf 3409 versus vtocl 3410. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1995. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.)

Assertion
Ref Expression
19.21v (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.21v
StepHypRef Expression
1 stdpc5v 2019 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
2 ax5e 1993 . . . 4 (∃𝑥𝜑𝜑)
32imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4 19.38 1914 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
53, 4syl 17 . 2 ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
61, 5impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  19.32v  2021  pm11.53v  2074  19.12vvv  2075  2sb6  2277  pm11.53  2341  19.12vv  2342  cbval2  2438  cbvaldva  2440  sbhb  2588  r2al  3088  r3al  3089  r19.21v  3109  ceqsralt  3381  rspc2gv  3471  euind  3545  reu2  3546  reuind  3563  unissb  4605  dfiin2g  4687  axrep5  4910  asymref  5653  fvn0ssdmfun  6493  dff13  6655  mpt22eqb  6916  findcard3  8359  marypha1lem  8495  marypha2lem3  8499  aceq1  9140  kmlem15  9188  cotr2g  13925  bnj864  31330  bnj865  31331  bnj978  31357  bnj1176  31411  bnj1186  31413  dfon2lem8  32031  dffun10  32358  bj-ssb1  32971  bj-ssbcom3lem  32987  bj-cbval2v  33073  bj-axrep5  33128  bj-ralcom4  33197  mpt2bi123f  34303  mptbi12f  34307  elmapintrab  38408  undmrnresiss  38436  dfhe3  38595  dffrege115  38798  ntrneiiso  38915  ntrneikb  38918  pm10.541  39092  pm10.542  39093  19.21vv  39101  pm11.62  39120  2sbc6g  39142  2rexsb  41690
  Copyright terms: Public domain W3C validator