Theorem 19.21v 1940

Description: Version of 19.21 2214 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 2214 and vtoclf 3521 versus vtocl 3515. 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  2310  pm11.53  2350  19.12vv  2351  sbhb  2525  r2al  3172  r3al  3174  ralcom4  3262  cbvraldva2  3318  ceqsralt  3475  rspc2gv  3586  elabgtOLD  3627  elabgtOLDOLD  3628  euind  3682  reu2  3683  reuind  3711  sbccomlem  3819  unissb  4896  dfiin2g  4986  axrep5  5232  asymref  6073  fvn0ssdmfun  7019  dff13  7200  mpo2eqb  7490  xpord3inddlem  8096  findcard3  9183  marypha1lem  9336  marypha2lem3  9340  aceq1  10027  kmlem15  10075  cotr2g  14899  bnj864  35078  bnj865  35079  bnj978  35105  bnj1176  35161  bnj1186  35163  dfon2lem8  35982  dffun10  36106  mpobi123f  38363  mptbi12f  38367  sn-axrep5v  42473  unielss  43460  elmapintrab  43817  undmrnresiss  43845  dfhe3  44016  dffrege115  44219  ntrneiiso  44332  ntrneikb  44335  pm10.541  44608  pm10.542  44609  19.21vv  44617  pm11.62  44635  2sbc6g  44656  2rexsb  47347