Theorem 19.21v 1972

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 1817) instead of a disjoint variable condition. For instance, 19.21v 1972 versus 19.21 2243 and vtoclf 3525 versus vtocl 3520. 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 1947. 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 1971	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1945	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 64	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1872	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 18	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.32v  1973  pm11.53v  1977  19.12vvv  2027  cbvaldvaw  2071  2sb6  2123  sbrimvwOLD  2129  sbal  2206  sbrim  2337  pm11.53  2375  19.12vv  2376  sbhb  2550  r2al  3198  r3al  3200  ralcom4  3288  ceqsralt  3484  rspc2gv  3586  elabgtOLD  3627  euind  3682  reu2  3683  reuind  3711  sbccomlem  3817  unissb  4901  dfiin2g  4989  axrep5  5240  asymref  6110  fvn0ssdmfun  7067  dff13  7251  mpo2eqb  7545  xpord3inddlem  8152  findcard3  9253  marypha1lem  9403  marypha2lem3  9407  aceq1  10120  kmlem15  10167  cotr2g  15049  bnj864  35431  bnj865  35432  bnj978  35458  bnj1176  35514  bnj1186  35516  dfon2lem8  36367  dffun10  36491  mh-unprimbi  37163  mpobi123f  38910  mptbi12f  38914  sn-axrep5v  43087  unielss  44059  elmapintrab  44416  undmrnresiss  44444  dfhe3  44615  dffrege115  44818  ntrneiiso  44931  ntrneikb  44934  pm10.541  45191  pm10.542  45192  19.21vv  45200  pm11.62  45218  2sbc6g  45239  2rexsb  47989