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

Theorem 19.21v 1855
 Description: Version of 19.21 2062 with a dv condition. 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 1701) instead of a dv condition. For instance, 19.21v 1855 versus 19.21 2062 and vtoclf 3231 versus vtocl 3232. 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 1830. 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 1854 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
2 ax5e 1829 . . . 4 (∃𝑥𝜑𝜑)
32imim1i 61 . . 3 ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4 19.38 1757 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
53, 4syl 17 . 2 ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
61, 5impbii 198 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  19.32v  1856  pm11.53v  1893  19.12vvv  1894  pm11.53  2167  19.12vv  2168  cbval2  2267  cbvaldva  2269  sbhb  2426  2sb6  2432  r2al  2923  r3al  2924  r19.21v  2943  ceqsralt  3202  euind  3360  reu2  3361  reuind  3378  unissb  4405  dfiin2g  4489  axrep5  4704  asymref  5431  fvn0ssdmfun  6258  dff13  6416  mpt22eqb  6667  findcard3  8088  marypha1lem  8222  marypha2lem3  8226  aceq1  8823  kmlem15  8869  cotr2g  13563  bnj864  30246  bnj865  30247  bnj978  30273  bnj1176  30327  bnj1186  30329  dfon2lem8  30939  dffun10  31191  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-cbval2v  31924  bj-axrep5  31980  bj-ralcom4  32062  mpt2bi123f  33141  mptbi12f  33145  elmapintrab  36901  undmrnresiss  36929  dfhe3  37089  dffrege115  37292  ntrneiiso  37409  ntrneikb  37412  pm10.541  37588  pm10.542  37589  19.21vv  37597  pm11.62  37616  2sbc6g  37638  2rexsb  39819
 Copyright terms: Public domain W3C validator