Theorem 19.21v 1940

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 non-freeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1786) instead of a disjoint variable condition. For instance, 19.21v 1940 versus 19.21 2205 and vtoclf 3476 versus vtocl 3477. 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 non-freeness hypothesis, by using nfv 1915. 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 1939	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1913	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1840	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃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 1911

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

This theorem is referenced by:  19.32v  1941  pm11.53v  1945  19.12vvv  1995  cbvaldvaw  2045  2sb6  2091  sbrimvw  2099  sbal  2163  hbsbw  2173  cbval2vOLD  2353  pm11.53  2356  19.12vv  2357  cbval2OLD  2422  sbhb  2540  r19.21v  3106  r2al  3130  r3al  3131  ralcom4  3162  cbvraldva2  3368  cbvrexdva2OLD  3370  ceqsralt  3444  rspc2gv  3550  euind  3638  reu2  3639  reuind  3667  unissb  4832  dfiin2g  4921  axrep5  5162  asymref  5948  fvn0ssdmfun  6833  dff13  7005  mpo2eqb  7278  findcard3  8794  marypha1lem  8930  marypha2lem3  8934  aceq1  9577  kmlem15  9624  cotr2g  14383  bnj864  32422  bnj865  32423  bnj978  32449  bnj1176  32505  bnj1186  32507  dfon2lem8  33282  dffun10  33765  wl-dfralv  35286  mpobi123f  35880  mptbi12f  35884  sn-axrep5v  39699  elmapintrab  40649  undmrnresiss  40677  dfhe3  40849  dffrege115  41052  ntrneiiso  41167  ntrneikb  41170  pm10.541  41444  pm10.542  41445  19.21vv  41453  pm11.62  41471  2sbc6g  41492  2rexsb  44024