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 1934
Description: Version of 19.21 2200 with a disjoint variable 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 1779) instead of a disjoint variable condition. For instance, 19.21v 1934 versus 19.21 2200 and vtoclf 3557 versus vtocl 3558. Note that "not free in" is less restrictive than "does not occur in". Note that the version with a disjoint variable condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1909. 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 1933 . 2 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
2 ax5e 1907 . . . 4 (∃𝑥𝜑𝜑)
32imim1i 63 . . 3 ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4 19.38 1833 . . 3 ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
53, 4syl 17 . 2 ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
61, 5impbii 211 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1529  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905
This theorem depends on definitions:  df-bi 209  df-ex 1775
This theorem is referenced by:  19.32v  1935  pm11.53v  1939  19.12vvv  1989  cbvaldvaw  2039  2sb6  2088  sbrimvw  2096  sbal  2159  cbval2vOLD  2358  pm11.53  2361  19.12vv  2362  cbval2OLD  2427  sbhb  2557  r19.21v  3173  r2al  3199  r3al  3200  ralcom4  3233  cbvraldva2  3455  cbvrexdva2OLD  3457  ceqsralt  3527  rspc2gv  3630  euind  3713  reu2  3714  reuind  3742  unissb  4861  dfiin2g  4948  axrep5  5187  asymref  5969  fvn0ssdmfun  6835  dff13  7005  mpo2eqb  7275  findcard3  8753  marypha1lem  8889  marypha2lem3  8893  aceq1  9535  kmlem15  9582  cotr2g  14328  bnj864  32187  bnj865  32188  bnj978  32214  bnj1176  32270  bnj1186  32272  dfon2lem8  33028  dffun10  33368  wl-dfralv  34833  mpobi123f  35432  mptbi12f  35436  sn-axrep5v  39099  elmapintrab  39927  undmrnresiss  39955  dfhe3  40112  dffrege115  40315  ntrneiiso  40432  ntrneikb  40435  pm10.541  40690  pm10.542  40691  19.21vv  40699  pm11.62  40717  2sbc6g  40738  2rexsb  43290
  Copyright terms: Public domain W3C validator