Theorem 19.21v 1941

Description: Version of 19.21 2215 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 1786) instead of a disjoint variable condition. For instance, 19.21v 1941 versus 19.21 2215 and vtoclf 3510 versus vtocl 3504. 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 1916. 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 1940	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1914	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1841	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  19.32v  1942  pm11.53v  1946  19.12vvv  1996  cbvaldvaw  2040  2sb6  2092  sbrimvw  2097  sbal  2175  hbsbwOLD  2178  sbrim  2311  pm11.53  2351  19.12vv  2352  sbhb  2526  r2al  3174  r3al  3176  ralcom4  3264  ceqsralt  3465  rspc2gv  3575  elabgtOLD  3616  elabgtOLDOLD  3617  euind  3671  reu2  3672  reuind  3700  sbccomlem  3808  unissb  4884  dfiin2g  4974  axrep5  5220  asymref  6073  fvn0ssdmfun  7020  dff13  7202  mpo2eqb  7492  xpord3inddlem  8097  findcard3  9186  marypha1lem  9339  marypha2lem3  9343  aceq1  10030  kmlem15  10078  cotr2g  14929  bnj864  35080  bnj865  35081  bnj978  35107  bnj1176  35163  bnj1186  35165  dfon2lem8  35986  dffun10  36110  mh-unprimbi  36742  mpobi123f  38497  mptbi12f  38501  sn-axrep5v  42672  unielss  43664  elmapintrab  44021  undmrnresiss  44049  dfhe3  44220  dffrege115  44423  ntrneiiso  44536  ntrneikb  44539  pm10.541  44812  pm10.542  44813  19.21vv  44821  pm11.62  44839  2sbc6g  44860  2rexsb  47561