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 3523 versus vtocl 3517. 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  cbvraldva2  3320  ceqsralt  3477  rspc2gv  3588  elabgtOLD  3629  elabgtOLDOLD  3630  euind  3684  reu2  3685  reuind  3713  sbccomlem  3821  unissb  4898  dfiin2g  4988  axrep5  5234  asymref  6081  fvn0ssdmfun  7028  dff13  7210  mpo2eqb  7500  xpord3inddlem  8106  findcard3  9195  marypha1lem  9348  marypha2lem3  9352  aceq1  10039  kmlem15  10087  cotr2g  14911  bnj864  35098  bnj865  35099  bnj978  35125  bnj1176  35181  bnj1186  35183  dfon2lem8  36004  dffun10  36128  mpobi123f  38413  mptbi12f  38417  sn-axrep5v  42589  unielss  43575  elmapintrab  43932  undmrnresiss  43960  dfhe3  44131  dffrege115  44334  ntrneiiso  44447  ntrneikb  44450  pm10.541  44723  pm10.542  44724  19.21vv  44732  pm11.62  44750  2sbc6g  44771  2rexsb  47461