Theorem 19.21v 1938

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 1782) instead of a disjoint variable condition. For instance, 19.21v 1938 versus 19.21 2208 and vtoclf 3576 versus vtocl 3570. 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 1913. 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 1937	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1911	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1837	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  19.32v  1939  pm11.53v  1943  19.12vvv  1988  cbvaldvaw  2037  2sb6  2086  sbrimvw  2091  sbal  2170  hbsbwOLD  2173  sbrim  2308  pm11.53  2352  19.12vv  2353  sbhb  2529  r19.21vOLD  3187  r2al  3201  r3al  3203  ralcom4  3292  ralcom4OLD  3293  nfra2wOLD  3306  cbvraldva2  3356  ceqsralt  3524  rspc2gv  3645  elabgt  3685  elabgtOLD  3686  euind  3746  reu2  3747  reuind  3775  sbccomlem  3891  unissb  4963  unissbOLD  4964  dfiin2g  5055  axrep5  5309  asymref  6148  fvn0ssdmfun  7108  dff13  7292  mpo2eqb  7582  xpord3inddlem  8195  findcard3  9346  findcard3OLD  9347  marypha1lem  9502  marypha2lem3  9506  aceq1  10186  kmlem15  10234  cotr2g  15025  bnj864  34898  bnj865  34899  bnj978  34925  bnj1176  34981  bnj1186  34983  dfon2lem8  35754  dffun10  35878  mpobi123f  38122  mptbi12f  38126  sn-axrep5v  42209  unielss  43179  elmapintrab  43538  undmrnresiss  43566  dfhe3  43737  dffrege115  43940  ntrneiiso  44053  ntrneikb  44056  pm10.541  44336  pm10.542  44337  19.21vv  44345  pm11.62  44363  2sbc6g  44384  2rexsb  47016