Theorem 19.21v 1937

Description: Version of 19.21 2205 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 1781) instead of a disjoint variable condition. For instance, 19.21v 1937 versus 19.21 2205 and vtoclf 3564 versus vtocl 3558. 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 1912. 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 1936	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1910	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1836	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  19.32v  1938  pm11.53v  1942  19.12vvv  1986  cbvaldvaw  2035  2sb6  2084  sbrimvw  2089  sbal  2167  hbsbwOLD  2170  sbrim  2303  pm11.53  2347  19.12vv  2348  sbhb  2524  r19.21vOLD  3179  r2al  3193  r3al  3195  ralcom4  3284  ralcom4OLD  3285  nfra2wOLD  3298  cbvraldva2  3346  ceqsralt  3514  rspc2gv  3632  elabgt  3672  elabgtOLD  3673  euind  3733  reu2  3734  reuind  3762  sbccomlem  3878  unissb  4944  unissbOLD  4945  dfiin2g  5037  axrep5  5293  asymref  6139  fvn0ssdmfun  7094  dff13  7275  mpo2eqb  7565  xpord3inddlem  8178  findcard3  9316  findcard3OLD  9317  marypha1lem  9471  marypha2lem3  9475  aceq1  10155  kmlem15  10203  cotr2g  15012  bnj864  34915  bnj865  34916  bnj978  34942  bnj1176  34998  bnj1186  35000  dfon2lem8  35772  dffun10  35896  mpobi123f  38149  mptbi12f  38153  sn-axrep5v  42234  unielss  43207  elmapintrab  43566  undmrnresiss  43594  dfhe3  43765  dffrege115  43968  ntrneiiso  44081  ntrneikb  44084  pm10.541  44363  pm10.542  44364  19.21vv  44372  pm11.62  44390  2sbc6g  44411  2rexsb  47051