Theorem 19.21v 1940

Description: Version of 19.21 2210 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 2210 and vtoclf 3517 versus vtocl 3511. 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  2089  sbrimvw  2094  sbal  2172  hbsbwOLD  2175  sbrim  2306  pm11.53  2346  19.12vv  2347  sbhb  2521  r2al  3168  r3al  3170  ralcom4  3258  cbvraldva2  3314  ceqsralt  3471  rspc2gv  3582  elabgtOLD  3623  elabgtOLDOLD  3624  euind  3678  reu2  3679  reuind  3707  sbccomlem  3815  unissb  4886  dfiin2g  4976  axrep5  5220  asymref  6058  fvn0ssdmfun  7002  dff13  7183  mpo2eqb  7473  xpord3inddlem  8079  findcard3  9162  marypha1lem  9312  marypha2lem3  9316  aceq1  10003  kmlem15  10051  cotr2g  14878  bnj864  34926  bnj865  34927  bnj978  34953  bnj1176  35009  bnj1186  35011  dfon2lem8  35824  dffun10  35948  mpobi123f  38202  mptbi12f  38206  sn-axrep5v  42249  unielss  43251  elmapintrab  43609  undmrnresiss  43637  dfhe3  43808  dffrege115  44011  ntrneiiso  44124  ntrneikb  44127  pm10.541  44400  pm10.542  44401  19.21vv  44409  pm11.62  44427  2sbc6g  44448  2rexsb  47132