Theorem 19.21v 1943

Description: Version of 19.21 2201 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 1787) instead of a disjoint variable condition. For instance, 19.21v 1943 versus 19.21 2201 and vtoclf 3498 versus vtocl 3499. 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 1918. 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 1942	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
2		ax5e 1916	. . . 4 ⊢ (∃𝑥𝜑 → 𝜑)
3	2	imim1i 63	. . 3 ⊢ ((𝜑 → ∀𝑥𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
4		19.38 1842	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
5	3, 4	syl 17	. 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
6	1, 5	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  19.32v  1944  pm11.53v  1948  19.12vvv  1993  cbvaldvaw  2042  2sb6  2090  sbrimvw  2095  sbal  2160  hbsbw  2170  sbrim  2302  cbval2vOLD  2342  pm11.53  2345  19.12vv  2346  sbhb  2526  r19.21vOLD  3115  r2al  3119  r3al  3120  nfra2wOLD  3156  ralcom4  3165  ralcom4OLD  3166  moel  3359  cbvraldva2  3393  ceqsralt  3464  rspc2gv  3570  elabgt  3604  euind  3660  reu2  3661  reuind  3689  unissb  4874  dfiin2g  4963  axrep5  5216  asymref  6026  fvn0ssdmfun  6961  dff13  7137  mpo2eqb  7415  findcard3  9066  marypha1lem  9201  marypha2lem3  9205  aceq1  9882  kmlem15  9929  cotr2g  14696  bnj864  32911  bnj865  32912  bnj978  32938  bnj1176  32994  bnj1186  32996  dfon2lem8  33775  dffun10  34225  mpobi123f  36329  mptbi12f  36333  sn-axrep5v  40192  elmapintrab  41191  undmrnresiss  41219  dfhe3  41390  dffrege115  41593  ntrneiiso  41708  ntrneikb  41711  pm10.541  41992  pm10.542  41993  19.21vv  42001  pm11.62  42019  2sbc6g  42040  2rexsb  44604