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

Theorem 19.21v 1865
 Description: Version of 19.21 2073 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 1707) instead of a dv condition. For instance, 19.21v 1865 versus 19.21 2073 and vtoclf 3247 versus vtocl 3248. 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 1840. 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 1864 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
2 ax5e 1838 . . . 4 (∃𝑥𝜑𝜑)
32imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4 19.38 1763 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
53, 4syl 17 . 2 ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
61, 5impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1478  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836 This theorem depends on definitions:  df-bi 197  df-ex 1702 This theorem is referenced by:  19.32v  1866  pm11.53v  1903  19.12vvv  1904  pm11.53  2178  19.12vv  2179  cbval2  2278  cbvaldva  2280  sbhb  2437  2sb6  2443  r2al  2934  r3al  2935  r19.21v  2955  ceqsralt  3218  rspc2gv  3309  euind  3379  reu2  3380  reuind  3397  unissb  4440  dfiin2g  4524  axrep5  4741  asymref  5476  fvn0ssdmfun  6311  dff13  6472  mpt22eqb  6729  findcard3  8154  marypha1lem  8290  marypha2lem3  8294  aceq1  8891  kmlem15  8937  cotr2g  13656  bnj864  30727  bnj865  30728  bnj978  30754  bnj1176  30808  bnj1186  30810  dfon2lem8  31423  dffun10  31690  bj-ssb1  32302  bj-ssbcom3lem  32319  bj-cbval2v  32406  bj-axrep5  32462  bj-ralcom4  32542  mpt2bi123f  33630  mptbi12f  33634  elmapintrab  37390  undmrnresiss  37418  dfhe3  37578  dffrege115  37781  ntrneiiso  37898  ntrneikb  37901  pm10.541  38075  pm10.542  38076  19.21vv  38084  pm11.62  38103  2sbc6g  38125  2rexsb  40495
 Copyright terms: Public domain W3C validator