Theorem 19.21v 1941

Description: Version of 19.21 2215 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 1786) instead of a disjoint variable condition. For instance, 19.21v 1941 versus 19.21 2215 and vtoclf 3509 versus vtocl 3503. 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 1916. 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 1940	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1914	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1841	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  19.32v  1942  pm11.53v  1946  19.12vvv  1996  cbvaldvaw  2040  2sb6  2092  sbrimvw  2097  sbal  2175  hbsbwOLD  2178  sbrim  2311  pm11.53  2350  19.12vv  2351  sbhb  2525  r2al  3173  r3al  3175  ralcom4  3263  ceqsralt  3464  rspc2gv  3574  elabgtOLD  3615  elabgtOLDOLD  3616  euind  3670  reu2  3671  reuind  3699  sbccomlem  3807  unissb  4883  dfiin2g  4973  axrep5  5220  asymref  6079  fvn0ssdmfun  7026  dff13  7209  mpo2eqb  7499  xpord3inddlem  8104  findcard3  9193  marypha1lem  9346  marypha2lem3  9350  aceq1  10039  kmlem15  10087  cotr2g  14938  bnj864  35064  bnj865  35065  bnj978  35091  bnj1176  35147  bnj1186  35149  dfon2lem8  35970  dffun10  36094  mh-unprimbi  36726  mpobi123f  38483  mptbi12f  38487  sn-axrep5v  42658  unielss  43646  elmapintrab  44003  undmrnresiss  44031  dfhe3  44202  dffrege115  44405  ntrneiiso  44518  ntrneikb  44521  pm10.541  44794  pm10.542  44795  19.21vv  44803  pm11.62  44821  2sbc6g  44842  2rexsb  47549