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 3506 versus vtocl 3507. 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  3142  r2al  3166  r3al  3167  ralcom4  3198  cbvraldva2  3403  cbvrexdva2OLD  3405  ceqsralt  3475  rspc2gv  3580  euind  3663  reu2  3664  reuind  3692  unissb  4832  dfiin2g  4919  axrep5  5160  asymref  5943  fvn0ssdmfun  6819  dff13  6991  mpo2eqb  7262  findcard3  8745  marypha1lem  8881  marypha2lem3  8885  aceq1  9528  kmlem15  9575  cotr2g  14327  bnj864  32304  bnj865  32305  bnj978  32331  bnj1176  32387  bnj1186  32389  dfon2lem8  33148  dffun10  33488  wl-dfralv  35006  mpobi123f  35600  mptbi12f  35604  sn-axrep5v  39400  elmapintrab  40276  undmrnresiss  40304  dfhe3  40476  dffrege115  40679  ntrneiiso  40794  ntrneikb  40797  pm10.541  41071  pm10.542  41072  19.21vv  41080  pm11.62  41098  2sbc6g  41119  2rexsb  43656