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 3533 versus vtocl 3527. 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  2304  pm11.53  2344  19.12vv  2345  sbhb  2520  r19.21vOLD  3160  r2al  3174  r3al  3176  ralcom4  3264  cbvraldva2  3323  ceqsralt  3485  rspc2gv  3601  elabgtOLD  3642  elabgtOLDOLD  3643  euind  3698  reu2  3699  reuind  3727  sbccomlem  3835  unissb  4906  unissbOLD  4907  dfiin2g  4999  axrep5  5245  asymref  6092  fvn0ssdmfun  7049  dff13  7232  mpo2eqb  7524  xpord3inddlem  8136  findcard3  9236  findcard3OLD  9237  marypha1lem  9391  marypha2lem3  9395  aceq1  10077  kmlem15  10125  cotr2g  14949  bnj864  34919  bnj865  34920  bnj978  34946  bnj1176  35002  bnj1186  35004  dfon2lem8  35785  dffun10  35909  mpobi123f  38163  mptbi12f  38167  sn-axrep5v  42211  unielss  43214  elmapintrab  43572  undmrnresiss  43600  dfhe3  43771  dffrege115  43974  ntrneiiso  44087  ntrneikb  44090  pm10.541  44363  pm10.542  44364  19.21vv  44372  pm11.62  44390  2sbc6g  44411  2rexsb  47106