Theorem 19.21v 1943

Description: Version of 19.21 2203 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 1788) instead of a disjoint variable condition. For instance, 19.21v 1943 versus 19.21 2203 and vtoclf 3487 versus vtocl 3488. 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 1783

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

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

This theorem is referenced by:  19.32v  1944  pm11.53v  1948  19.12vvv  1993  cbvaldvaw  2042  2sb6  2090  sbrimvw  2096  sbal  2161  hbsbw  2171  cbval2vOLD  2343  pm11.53  2346  19.12vv  2347  sbhb  2525  r19.21v  3100  r2al  3124  r3al  3125  nfra2wOLD  3152  ralcom4  3161  ralcom4OLD  3162  cbvraldva2  3381  ceqsralt  3453  rspc2gv  3561  elabgt  3596  euind  3654  reu2  3655  reuind  3683  unissb  4870  dfiin2g  4958  axrep5  5211  asymref  6010  fvn0ssdmfun  6934  dff13  7109  mpo2eqb  7384  findcard3  8987  marypha1lem  9122  marypha2lem3  9126  aceq1  9804  kmlem15  9851  cotr2g  14615  bnj864  32802  bnj865  32803  bnj978  32829  bnj1176  32885  bnj1186  32887  dfon2lem8  33672  dffun10  34143  mpobi123f  36247  mptbi12f  36251  sn-axrep5v  40113  elmapintrab  41073  undmrnresiss  41101  dfhe3  41272  dffrege115  41475  ntrneiiso  41590  ntrneikb  41593  pm10.541  41874  pm10.542  41875  19.21vv  41883  pm11.62  41901  2sbc6g  41922  2rexsb  44480