Theorem 19.21v 1855

Description: Version of 19.21 2062 with a dv condition.

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 1701) instead of a dv condition. For instance, 19.21v 1855 versus 19.21 2062 and vtoclf 3231 versus vtocl 3232. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1830. 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 1854	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1829	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 61	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1757	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 198	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  19.32v  1856  pm11.53v  1893  19.12vvv  1894  pm11.53  2167  19.12vv  2168  cbval2  2267  cbvaldva  2269  sbhb  2426  2sb6  2432  r2al  2923  r3al  2924  r19.21v  2943  ceqsralt  3202  euind  3360  reu2  3361  reuind  3378  unissb  4405  dfiin2g  4489  axrep5  4704  asymref  5431  fvn0ssdmfun  6258  dff13  6416  mpt22eqb  6667  findcard3  8088  marypha1lem  8222  marypha2lem3  8226  aceq1  8823  kmlem15  8869  cotr2g  13563  bnj864  30246  bnj865  30247  bnj978  30273  bnj1176  30327  bnj1186  30329  dfon2lem8  30939  dffun10  31191  bj-ssb1  31822  bj-ssbcom3lem  31839  bj-cbval2v  31924  bj-axrep5  31980  bj-ralcom4  32062  mpt2bi123f  33141  mptbi12f  33145  elmapintrab  36901  undmrnresiss  36929  dfhe3  37089  dffrege115  37292  ntrneiiso  37409  ntrneikb  37412  pm10.541  37588  pm10.542  37589  19.21vv  37597  pm11.62  37616  2sbc6g  37638  2rexsb  39819