Theorem 19.21v 1946

Description: Version of 19.21 2219 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 1791) instead of a disjoint variable condition. For instance, 19.21v 1946 versus 19.21 2219 and vtoclf 3509 versus vtocl 3503. 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 1921. 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 1945	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1919	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1846	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 210	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  19.32v  1947  pm11.53v  1951  19.12vvv  2001  cbvaldvaw  2045  2sb6  2097  sbrimvw  2102  sbal  2180  sbrim  2315  pm11.53  2354  19.12vv  2355  sbhb  2529  r2al  3175  r3al  3177  ralcom4  3265  ceqsralt  3465  rspc2gv  3570  elabgtOLD  3611  euind  3665  reu2  3666  reuind  3694  sbccomlem  3801  unissb  4871  dfiin2g  4960  axrep5  5207  asymref  6066  fvn0ssdmfun  7015  dff13  7198  mpo2eqb  7488  xpord3inddlem  8094  findcard3  9183  marypha1lem  9336  marypha2lem3  9340  aceq1  10030  kmlem15  10078  cotr2g  14929  bnj864  35104  bnj865  35105  bnj978  35131  bnj1176  35187  bnj1186  35189  dfon2lem8  36016  dffun10  36140  mh-unprimbi  36772  mpobi123f  38529  mptbi12f  38533  sn-axrep5v  42704  unielss  43663  elmapintrab  44020  undmrnresiss  44048  dfhe3  44219  dffrege115  44422  ntrneiiso  44535  ntrneikb  44538  pm10.541  44811  pm10.542  44812  19.21vv  44820  pm11.62  44838  2sbc6g  44859  2rexsb  47564