Theorem 19.21v 1940

Description: Version of 19.21 2212 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 1785) instead of a disjoint variable condition. For instance, 19.21v 1940 versus 19.21 2212 and vtoclf 3519 versus vtocl 3513. 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 1915. 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 1939	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1913	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1840	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  19.32v  1941  pm11.53v  1945  19.12vvv  1995  cbvaldvaw  2039  2sb6  2091  sbrimvw  2096  sbal  2174  hbsbwOLD  2177  sbrim  2308  pm11.53  2348  19.12vv  2349  sbhb  2523  r2al  3170  r3al  3172  ralcom4  3260  cbvraldva2  3316  ceqsralt  3473  rspc2gv  3584  elabgtOLD  3625  elabgtOLDOLD  3626  euind  3680  reu2  3681  reuind  3709  sbccomlem  3817  unissb  4894  dfiin2g  4984  axrep5  5230  asymref  6071  fvn0ssdmfun  7017  dff13  7198  mpo2eqb  7488  xpord3inddlem  8094  findcard3  9181  marypha1lem  9334  marypha2lem3  9338  aceq1  10025  kmlem15  10073  cotr2g  14897  bnj864  35027  bnj865  35028  bnj978  35054  bnj1176  35110  bnj1186  35112  dfon2lem8  35931  dffun10  36055  mpobi123f  38302  mptbi12f  38306  sn-axrep5v  42414  unielss  43402  elmapintrab  43759  undmrnresiss  43787  dfhe3  43958  dffrege115  44161  ntrneiiso  44274  ntrneikb  44277  pm10.541  44550  pm10.542  44551  19.21vv  44559  pm11.62  44577  2sbc6g  44598  2rexsb  47289