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 3560 versus vtocl 3561. 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  3177  r2al  3203  r3al  3204  ralcom4  3237  cbvraldva2  3458  cbvrexdva2OLD  3460  ceqsralt  3530  rspc2gv  3634  euind  3717  reu2  3718  reuind  3746  unissb  4872  dfiin2g  4959  axrep5  5198  asymref  5978  fvn0ssdmfun  6844  dff13  7015  mpo2eqb  7285  findcard3  8763  marypha1lem  8899  marypha2lem3  8903  aceq1  9545  kmlem15  9592  cotr2g  14338  bnj864  32196  bnj865  32197  bnj978  32223  bnj1176  32279  bnj1186  32281  dfon2lem8  33037  dffun10  33377  wl-dfralv  34843  mpobi123f  35442  mptbi12f  35446  sn-axrep5v  39115  elmapintrab  39943  undmrnresiss  39971  dfhe3  40128  dffrege115  40331  ntrneiiso  40448  ntrneikb  40451  pm10.541  40706  pm10.542  40707  19.21vv  40715  pm11.62  40733  2sbc6g  40754  2rexsb  43306