Theorem 19.23v 1941

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  19.23vv  1942  pm11.53v  1943  equsv  2001  sb4b  2479  2mo2  2646  ceqsalv  3520  clel2g  3658  clel4g  3662  elabd2  3669  elabgt  3671  elabgtOLD  3672  elabg  3675  euind  3729  reuind  3758  sbcg  3862  ralsng  4674  snssb  4781  unissb  4938  unissbOLD  4939  disjor  5124  dftr2  5260  ssrelrel  5805  cotrg  6126  cotrgOLD  6127  cotrgOLDOLD  6128  dffun2OLDOLD  6572  fununi  6640  dff13  7276  dffi2  9464  aceq2  10160  psgnunilem4  19516  metcld  25341  metcld2  25342  isch2  31243  disjorf  32593  funcnv5mpt  32679  bnj1052  34990  bnj1030  35002  dfon2lem8  35792  bj-ssbeq  36655  bj-ssbid2ALT  36665  bj-sblem1  36844  bj-sblem2  36845  bj-sblem  36846  wl-equsalvw  37540  ineleq  38356  cocossss  38438  cossssid3  38471  trcoss2  38486  elmapintrab  43594  elinintrab  43595  undmrnresiss  43622  elintima  43671  relexp0eq  43719  dfhe3  43793  ismnuprim  44318  pm10.52  44389  truniALT  44566  tpid3gVD  44867  truniALTVD  44903  onfrALTVD  44916  unisnALT  44951