Theorem 19.21v 1966

Description: Version of 19.21 2249 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 1811) instead of a disjoint variable condition. For instance, 19.21v 1966 versus 19.21 2249 and vtoclf 3539 versus vtocl 3534. 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 1941. 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 1965	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1939	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 64	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1866	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 18	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

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

This theorem is referenced by:  19.32v  1967  pm11.53v  1971  19.12vvv  2021  cbvaldvaw  2065  2sb6  2126  sbrimvwOLD  2132  sbal  2210  sbrim  2345  pm11.53  2384  19.12vv  2385  sbhb  2559  r2al  3207  r3al  3209  ralcom4  3297  ceqsralt  3497  rspc2gv  3600  elabgtOLD  3641  euind  3696  reu2  3697  reuind  3725  sbccomlem  3831  unissb  4907  dfiin2g  4996  axrep5  5247  asymref  6114  fvn0ssdmfun  7067  dff13  7250  mpo2eqb  7540  xpord3inddlem  8146  findcard3  9239  marypha1lem  9389  marypha2lem3  9393  aceq1  10097  kmlem15  10144  cotr2g  15009  bnj864  35251  bnj865  35252  bnj978  35278  bnj1176  35334  bnj1186  35336  dfon2lem8  36175  dffun10  36299  mh-unprimbi  36940  mpobi123f  38696  mptbi12f  38700  sn-axrep5v  42873  unielss  43832  elmapintrab  44189  undmrnresiss  44217  dfhe3  44388  dffrege115  44591  ntrneiiso  44704  ntrneikb  44707  pm10.541  44964  pm10.542  44965  19.21vv  44973  pm11.62  44991  2sbc6g  45012  2rexsb  47722