Theorem 19.21v 1940

Description: Version of 19.21 2207 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 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 1785) instead of a disjoint variable condition. For instance, 19.21v 1940 versus 19.21 2207 and vtoclf 3558 versus vtocl 3559. 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 non-freeness 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 1839	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 211	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  ∃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 209  df-ex 1781

This theorem is referenced by:  19.32v  1941  pm11.53v  1945  19.12vvv  1995  cbvaldvaw  2045  2sb6  2094  sbrimvw  2102  sbal  2166  cbval2vOLD  2364  pm11.53  2367  19.12vv  2368  cbval2OLD  2433  sbhb  2563  r19.21v  3175  r2al  3201  r3al  3202  ralcom4  3235  cbvraldva2  3456  cbvrexdva2OLD  3458  ceqsralt  3528  rspc2gv  3632  euind  3715  reu2  3716  reuind  3744  unissb  4870  dfiin2g  4957  axrep5  5196  asymref  5976  fvn0ssdmfun  6842  dff13  7013  mpo2eqb  7283  findcard3  8761  marypha1lem  8897  marypha2lem3  8901  aceq1  9543  kmlem15  9590  cotr2g  14336  bnj864  32194  bnj865  32195  bnj978  32221  bnj1176  32277  bnj1186  32279  dfon2lem8  33035  dffun10  33375  wl-dfralv  34856  mpobi123f  35455  mptbi12f  35459  sn-axrep5v  39157  elmapintrab  39985  undmrnresiss  40013  dfhe3  40170  dffrege115  40373  ntrneiiso  40490  ntrneikb  40493  pm10.541  40748  pm10.542  40749  19.21vv  40757  pm11.62  40775  2sbc6g  40796  2rexsb  43348