Theorem 19.21v 1942

Description: Version of 19.21 2200 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 1786) instead of a disjoint variable condition. For instance, 19.21v 1942 versus 19.21 2200 and vtoclf 3547 versus vtocl 3549. 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 1917. 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 1941	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1915	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1841	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  19.32v  1943  pm11.53v  1947  19.12vvv  1992  cbvaldvaw  2041  2sb6  2089  sbrimvw  2094  sbal  2159  hbsbw  2169  sbrim  2300  pm11.53  2342  19.12vv  2343  sbhb  2520  r19.21vOLD  3180  r2al  3194  r3al  3196  ralcom4  3283  ralcom4OLD  3284  nfra2wOLD  3297  cbvraldva2  3344  ceqsralt  3506  rspc2gv  3620  elabgt  3661  euind  3719  reu2  3720  reuind  3748  unissb  4942  unissbOLD  4943  dfiin2g  5034  axrep5  5290  asymref  6114  fvn0ssdmfun  7073  dff13  7250  mpo2eqb  7537  xpord3inddlem  8136  findcard3  9281  findcard3OLD  9282  marypha1lem  9424  marypha2lem3  9428  aceq1  10108  kmlem15  10155  cotr2g  14919  bnj864  33921  bnj865  33922  bnj978  33948  bnj1176  34004  bnj1186  34006  dfon2lem8  34750  dffun10  34874  mpobi123f  37018  mptbi12f  37022  sn-axrep5v  41029  unielss  41952  elmapintrab  42312  undmrnresiss  42340  dfhe3  42511  dffrege115  42714  ntrneiiso  42827  ntrneikb  42830  pm10.541  43111  pm10.542  43112  19.21vv  43120  pm11.62  43138  2sbc6g  43159  2rexsb  45795