Theorem 19.21v 1971

Description: Version of 19.21 2243 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 nonfreeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a nonfreeness hypothesis ("f" stands for "not free in", see df-nf 1816) instead of a disjoint variable condition. For instance, 19.21v 1971 versus 19.21 2243 and vtoclf 3525 versus vtocl 3520. 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 nonfreeness hypothesis, by using nfv 1946. 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

Step	Hyp	Ref	Expression
1		stdpc5v 1970	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1944	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 64	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1871	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 18	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  19.32v  1972  pm11.53v  1976  19.12vvv  2026  cbvaldvaw  2070  2sb6  2122  sbrimvwOLD  2128  sbal  2205  sbrim  2337  pm11.53  2375  19.12vv  2376  sbhb  2550  r2al  3198  r3al  3200  ralcom4  3288  ceqsralt  3484  rspc2gv  3585  elabgtOLD  3626  euind  3681  reu2  3682  reuind  3710  sbccomlem  3817  unissb  4900  dfiin2g  4988  axrep5  5238  asymref  6111  fvn0ssdmfun  7077  dff13  7260  mpo2eqb  7554  xpord3inddlem  8175  findcard3  9279  marypha1lem  9430  marypha2lem3  9434  aceq1  10201  kmlem15  10248  cotr2g  15136  bnj864  35600  bnj865  35601  bnj978  35627  bnj1176  35683  bnj1186  35685  dfon2lem8  36646  dffun10  36770  mh-unprimbi  37426  mpobi123f  39201  mptbi12f  39205  sn-axrep5v  43378  unielss  44327  elmapintrab  44684  undmrnresiss  44711  dfhe3  44882  dffrege115  45085  ntrneiiso  45198  ntrneikb  45201  pm10.541  45458  pm10.542  45459  19.21vv  45467  pm11.62  45485  2sbc6g  45506  2rexsb  48278