Theorem 19.23v 1943

Description: Version of 19.23 2218 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 1968. (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 1835	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1913	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1911	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1840	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  19.23vv  1944  pm11.53v  1945  equsv  2004  sb4b  2479  2mo2  2647  ceqsalv  3480  clel2g  3613  clel4g  3617  elabd2  3624  elabgt  3626  elabgtOLD  3627  elabgtOLDOLD  3628  euind  3682  reuind  3711  sbcg  3813  ralsng  4632  snssb  4739  unissb  4896  disjor  5080  dftr2  5207  ssrelrel  5745  cotrg  6068  fununi  6567  dff13  7200  dffi2  9326  aceq2  10029  psgnunilem4  19426  metcld  25262  metcld2  25263  isch2  31298  disjorf  32654  funcnv5mpt  32746  bnj1052  35131  bnj1030  35143  dfon2lem8  35982  bj-ssbeq  36854  bj-ssbid2ALT  36864  bj-sblem1  37043  bj-sblem2  37044  bj-sblem  37045  wl-equsalvw  37743  ineleq  38547  cocossss  38699  cossssid3  38732  trcoss2  38747  elmapintrab  43817  elinintrab  43818  undmrnresiss  43845  elintima  43894  relexp0eq  43942  dfhe3  44016  ismnuprim  44535  pm10.52  44606  truniALT  44782  tpid3gVD  45082  truniALTVD  45118  onfrALTVD  45131  unisnALT  45166