Theorem 19.21v 1908

Description: Version of 19.21 2113 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 1750) instead of a dv condition. For instance, 19.21v 1908 versus 19.21 2113 and vtoclf 3289 versus vtocl 3290. 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 1883. 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 1907	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1881	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1806	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 199	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-ex 1745

This theorem is referenced by:  19.32v  1909  pm11.53v  1962  19.12vvv  1963  pm11.53  2215  19.12vv  2216  cbval2  2315  cbvaldva  2317  sbhb  2466  2sb6  2472  r2al  2968  r3al  2969  r19.21v  2989  ceqsralt  3260  rspc2gv  3352  euind  3426  reu2  3427  reuind  3444  unissb  4501  dfiin2g  4585  axrep5  4809  asymref  5547  fvn0ssdmfun  6390  dff13  6552  mpt22eqb  6811  findcard3  8244  marypha1lem  8380  marypha2lem3  8384  aceq1  8978  kmlem15  9024  cotr2g  13761  bnj864  31118  bnj865  31119  bnj978  31145  bnj1176  31199  bnj1186  31201  dfon2lem8  31819  dffun10  32146  bj-ssb1  32758  bj-ssbcom3lem  32775  bj-cbval2v  32862  bj-axrep5  32917  bj-ralcom4  32993  mpt2bi123f  34101  mptbi12f  34105  elmapintrab  38199  undmrnresiss  38227  dfhe3  38386  dffrege115  38589  ntrneiiso  38706  ntrneikb  38709  pm10.541  38883  pm10.542  38884  19.21vv  38892  pm11.62  38911  2sbc6g  38933  2rexsb  41491