Theorem 19.21v 1943

Description: Version of 19.21 2201 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 1787) instead of a disjoint variable condition. For instance, 19.21v 1943 versus 19.21 2201 and vtoclf 3548 versus vtocl 3550. 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 1918. 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 1942	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1916	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1842	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  19.32v  1944  pm11.53v  1948  19.12vvv  1993  cbvaldvaw  2042  2sb6  2090  sbrimvw  2095  sbal  2160  hbsbw  2170  sbrim  2301  pm11.53  2343  19.12vv  2344  sbhb  2521  r19.21vOLD  3181  r2al  3195  r3al  3197  ralcom4  3284  ralcom4OLD  3285  nfra2wOLD  3298  cbvraldva2  3345  ceqsralt  3507  rspc2gv  3622  elabgt  3663  euind  3721  reu2  3722  reuind  3750  unissb  4944  unissbOLD  4945  dfiin2g  5036  axrep5  5292  asymref  6118  fvn0ssdmfun  7077  dff13  7254  mpo2eqb  7541  xpord3inddlem  8140  findcard3  9285  findcard3OLD  9286  marypha1lem  9428  marypha2lem3  9432  aceq1  10112  kmlem15  10159  cotr2g  14923  bnj864  33964  bnj865  33965  bnj978  33991  bnj1176  34047  bnj1186  34049  dfon2lem8  34793  dffun10  34917  mpobi123f  37078  mptbi12f  37082  sn-axrep5v  41081  unielss  42015  elmapintrab  42375  undmrnresiss  42403  dfhe3  42574  dffrege115  42777  ntrneiiso  42890  ntrneikb  42893  pm10.541  43174  pm10.542  43175  19.21vv  43183  pm11.62  43201  2sbc6g  43222  2rexsb  45857