Theorem 19.21v 1939

Description: Version of 19.21 2208 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 1784) instead of a disjoint variable condition. For instance, 19.21v 1939 versus 19.21 2208 and vtoclf 3548 versus vtocl 3542. 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 1914. 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 1938	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1912	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1839	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  19.32v  1940  pm11.53v  1944  19.12vvv  1994  cbvaldvaw  2038  2sb6  2087  sbrimvw  2092  sbal  2170  hbsbwOLD  2173  sbrim  2305  pm11.53  2348  19.12vv  2349  sbhb  2526  r19.21vOLD  3167  r2al  3181  r3al  3183  ralcom4  3272  cbvraldva2  3331  ceqsralt  3500  rspc2gv  3616  elabgt  3656  elabgtOLD  3657  euind  3712  reu2  3713  reuind  3741  sbccomlem  3849  unissb  4920  unissbOLD  4921  dfiin2g  5013  axrep5  5262  asymref  6110  fvn0ssdmfun  7069  dff13  7252  mpo2eqb  7544  xpord3inddlem  8158  findcard3  9295  findcard3OLD  9296  marypha1lem  9450  marypha2lem3  9454  aceq1  10136  kmlem15  10184  cotr2g  15000  bnj864  34958  bnj865  34959  bnj978  34985  bnj1176  35041  bnj1186  35043  dfon2lem8  35813  dffun10  35937  mpobi123f  38191  mptbi12f  38195  sn-axrep5v  42234  unielss  43209  elmapintrab  43567  undmrnresiss  43595  dfhe3  43766  dffrege115  43969  ntrneiiso  44082  ntrneikb  44085  pm10.541  44358  pm10.542  44359  19.21vv  44367  pm11.62  44385  2sbc6g  44406  2rexsb  47097