Theorem 19.21v 1958

Description: Version of 19.21 2241 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 1803) instead of a disjoint variable condition. For instance, 19.21v 1958 versus 19.21 2241 and vtoclf 3529 versus vtocl 3524. 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 1933. 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 1957	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1931	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1858	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 211	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  19.32v  1959  pm11.53v  1963  19.12vvv  2013  cbvaldvaw  2057  2sb6  2118  sbrimvwOLD  2124  sbal  2202  sbrim  2337  pm11.53  2376  19.12vv  2377  sbhb  2551  r2al  3197  r3al  3199  ralcom4  3287  ceqsralt  3487  rspc2gv  3590  elabgtOLD  3631  euind  3685  reu2  3686  reuind  3714  sbccomlem  3820  unissb  4896  dfiin2g  4985  axrep5  5232  asymref  6099  fvn0ssdmfun  7050  dff13  7233  mpo2eqb  7523  xpord3inddlem  8128  findcard3  9221  marypha1lem  9373  marypha2lem3  9377  aceq1  10067  kmlem15  10115  cotr2g  14983  bnj864  35178  bnj865  35179  bnj978  35205  bnj1176  35261  bnj1186  35263  dfon2lem8  36099  dffun10  36223  mh-unprimbi  36865  mpobi123f  38622  mptbi12f  38626  sn-axrep5v  42797  unielss  43756  elmapintrab  44113  undmrnresiss  44141  dfhe3  44312  dffrege115  44515  ntrneiiso  44628  ntrneikb  44631  pm10.541  44904  pm10.542  44905  19.21vv  44913  pm11.62  44931  2sbc6g  44952  2rexsb  47656