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 2023
Description: Version of 19.21 2234 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 1861) instead of a dv condition. For instance, 19.21v 2023 versus 19.21 2234 and vtoclf 3414 versus vtocl 3415. 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 1998. 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 2022 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
2 ax5e 1996 . . . 4 (∃𝑥𝜑𝜑)
32imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4 19.38 1917 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
53, 4syl 17 . 2 ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
61, 5impbii 200 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1632  wex 1855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994
This theorem depends on definitions:  df-bi 198  df-ex 1856
This theorem is referenced by:  19.32v  2024  pm11.53v  2077  19.12vvv  2078  2sb6  2280  pm11.53  2344  19.12vv  2345  cbval2  2441  cbvaldva  2443  sbhb  2591  r2al  3091  r3al  3092  r19.21v  3112  ceqsralt  3386  rspc2gv  3477  euind  3551  reu2  3552  reuind  3569  unissb  4616  dfiin2g  4698  axrep5  4923  asymref  5664  fvn0ssdmfun  6510  dff13  6674  mpt22eqb  6937  findcard3  8380  marypha1lem  8516  marypha2lem3  8520  aceq1  9161  kmlem15  9209  cotr2g  13947  bnj864  31347  bnj865  31348  bnj978  31374  bnj1176  31428  bnj1186  31430  dfon2lem8  32048  dffun10  32375  bj-ssb1  32987  bj-ssbcom3lem  33003  bj-cbval2v  33089  bj-axrep5  33144  bj-ralcom4  33214  mpt2bi123f  34319  mptbi12f  34323  elmapintrab  38422  undmrnresiss  38450  dfhe3  38609  dffrege115  38812  ntrneiiso  38929  ntrneikb  38932  pm10.541  39106  pm10.542  39107  19.21vv  39115  pm11.62  39134  2sbc6g  39155  2rexsb  41716
  Copyright terms: Public domain W3C validator