Theorem 19.23v 1949

Description: Version of 19.23 2223 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 1974. (Revised by Rohan Ridenour, 15-Apr-2022.)

Assertion

Ref	Expression
19.23v	⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		exim 1841	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1919	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1917	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1846	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	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.23vv  1950  pm11.53v  1951  equsv  2010  sb4b  2483  2mo2  2651  ceqsalv  3470  clel2g  3597  clel4g  3601  elabd2  3608  elabgt  3610  elabgtOLD  3611  euind  3665  reuind  3694  sbcg  3795  ralsng  4607  snssb  4714  unissb  4871  disjor  5054  dftr2  5181  ssrelrel  5739  cotrg  6061  fununi  6560  dff13  7198  dffi2  9326  aceq2  10032  psgnunilem4  19463  metcld  25291  metcld2  25292  isch2  31312  disjorf  32668  funcnv5mpt  32759  bnj1052  35157  bnj1030  35169  dfon2lem8  36016  mh-unprimbi  36772  mh-infprim1bi  36774  bj-ssbeq  36993  bj-ssbid2ALT  37003  bj-sblem1  37195  bj-sblem2  37196  bj-sblem  37197  wl-equsalvw  37909  ineleq  38721  cocossss  38893  cossssid3  38926  trcoss2  38941  elmapintrab  44020  elinintrab  44021  undmrnresiss  44048  elintima  44097  relexp0eq  44145  dfhe3  44219  ismnuprim  44738  pm10.52  44809  truniALT  44985  tpid3gVD  45285  truniALTVD  45321  onfrALTVD  45334  unisnALT  45369