Theorem 19.21v 1982

Description: Version of 19.21 2191 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 1828) instead of a disjoint variable condition. For instance, 19.21v 1982 versus 19.21 2191 and vtoclf 3458 versus vtocl 3459. 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 1957. 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 1981	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1955	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1882	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 201	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599  ∃wex 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  19.32v  1983  pm11.53v  1987  19.12vvv  2037  2sb6  2252  pm11.53  2314  19.12vv  2315  cbval2  2373  cbvaldva  2375  sbhb  2517  r2al  3120  r3al  3121  r19.21v  3141  ceqsralt  3430  rspc2gv  3522  euind  3604  reu2  3605  reuind  3627  unissb  4704  dfiin2g  4786  axrep5  5012  asymref  5767  fvn0ssdmfun  6614  dff13  6784  mpt22eqb  7046  findcard3  8491  marypha1lem  8627  marypha2lem3  8631  aceq1  9273  kmlem15  9321  cotr2g  14124  bnj864  31605  bnj865  31606  bnj978  31632  bnj1176  31686  bnj1186  31688  dfon2lem8  32297  dffun10  32624  bj-ssb1  33238  bj-ssbcom3lem  33254  bj-cbval2v  33336  bj-axrep5  33383  bj-ralcom4  33452  wl-dfralv  33985  mpt2bi123f  34587  mptbi12f  34591  elmapintrab  38831  undmrnresiss  38859  dfhe3  39017  dffrege115  39220  ntrneiiso  39337  ntrneikb  39340  pm10.541  39514  pm10.542  39515  19.21vv  39523  pm11.62  39542  2sbc6g  39563  2rexsb  42121