Theorem 19.21v 1972

Description: Version of 19.21 2244 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 2244 and vtoclf 3526 versus vtocl 3521. 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  2338  pm11.53  2376  19.12vv  2377  sbhb  2551  r2al  3199  r3al  3201  ralcom4  3289  ceqsralt  3485  rspc2gv  3586  elabgtOLD  3627  euind  3682  reu2  3683  reuind  3711  sbccomlem  3817  unissb  4901  dfiin2g  4989  axrep5  5239  asymref  6110  fvn0ssdmfun  7074  dff13  7258  mpo2eqb  7552  xpord3inddlem  8171  findcard3  9274  marypha1lem  9425  marypha2lem3  9429  aceq1  10196  kmlem15  10243  cotr2g  15129  bnj864  35552  bnj865  35553  bnj978  35579  bnj1176  35635  bnj1186  35637  dfon2lem8  36552  dffun10  36676  mh-unprimbi  37332  mpobi123f  39094  mptbi12f  39098  sn-axrep5v  43271  unielss  44219  elmapintrab  44576  undmrnresiss  44603  dfhe3  44774  dffrege115  44977  ntrneiiso  45090  ntrneikb  45093  pm10.541  45350  pm10.542  45351  19.21vv  45359  pm11.62  45377  2sbc6g  45398  2rexsb  48170