Theorem 19.21v 1969

Description: Version of 19.21 2243 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 1814) instead of a disjoint variable condition. For instance, 19.21v 1969 versus 19.21 2243 and vtoclf 3530 versus vtocl 3525. 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 1944. 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 1968	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1942	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 64	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1869	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 18	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  19.32v  1970  pm11.53v  1974  19.12vvv  2024  cbvaldvaw  2068  2sb6  2120  sbrimvwOLD  2126  sbal  2204  sbrim  2339  pm11.53  2378  19.12vv  2379  sbhb  2553  r2al  3201  r3al  3203  ralcom4  3291  ceqsralt  3489  rspc2gv  3591  elabgtOLD  3632  euind  3687  reu2  3688  reuind  3716  sbccomlem  3822  unissb  4906  dfiin2g  4995  axrep5  5246  asymref  6116  fvn0ssdmfun  7069  dff13  7252  mpo2eqb  7542  xpord3inddlem  8146  findcard3  9239  marypha1lem  9389  marypha2lem3  9393  aceq1  10097  kmlem15  10144  cotr2g  15009  bnj864  35310  bnj865  35311  bnj978  35337  bnj1176  35393  bnj1186  35395  dfon2lem8  36280  dffun10  36404  mh-unprimbi  37055  mpobi123f  38811  mptbi12f  38815  sn-axrep5v  42988  unielss  43945  elmapintrab  44302  undmrnresiss  44330  dfhe3  44501  dffrege115  44704  ntrneiiso  44817  ntrneikb  44820  pm10.541  45077  pm10.542  45078  19.21vv  45086  pm11.62  45104  2sbc6g  45125  2rexsb  47838