Theorem 19.21v 1934

Description: Version of 19.21 2192 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 1778) instead of a disjoint variable condition. For instance, 19.21v 1934 versus 19.21 2192 and vtoclf 3544 versus vtocl 3538. 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 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

Step	Hyp	Ref	Expression
1		stdpc5v 1933	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1907	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1833	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-ex 1774

This theorem is referenced by:  19.32v  1935  pm11.53v  1939  19.12vvv  1984  cbvaldvaw  2033  2sb6  2081  sbrimvw  2086  sbal  2151  hbsbw  2161  sbrim  2292  pm11.53  2334  19.12vv  2335  sbhb  2512  r19.21vOLD  3172  r2al  3186  r3al  3188  ralcom4  3275  ralcom4OLD  3276  nfra2wOLD  3289  cbvraldva2  3336  ceqsralt  3499  rspc2gv  3613  elabgt  3654  euind  3712  reu2  3713  reuind  3741  unissb  4933  unissbOLD  4934  dfiin2g  5025  axrep5  5281  asymref  6107  fvn0ssdmfun  7066  dff13  7246  mpo2eqb  7533  xpord3inddlem  8134  findcard3  9280  findcard3OLD  9281  marypha1lem  9423  marypha2lem3  9427  aceq1  10107  kmlem15  10154  cotr2g  14919  bnj864  34388  bnj865  34389  bnj978  34415  bnj1176  34471  bnj1186  34473  dfon2lem8  35223  dffun10  35347  mpobi123f  37486  mptbi12f  37490  sn-axrep5v  41492  unielss  42422  elmapintrab  42782  undmrnresiss  42810  dfhe3  42981  dffrege115  43184  ntrneiiso  43297  ntrneikb  43300  pm10.541  43581  pm10.542  43582  19.21vv  43590  pm11.62  43608  2sbc6g  43629  2rexsb  46260