Theorem 19.23v 1943

Description: Version of 19.23 2216 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  2477  2mo2  2645  ceqsalv  3478  clel2g  3611  clel4g  3615  elabd2  3622  elabgt  3624  elabgtOLD  3625  elabgtOLDOLD  3626  euind  3680  reuind  3709  sbcg  3811  ralsng  4630  snssb  4737  unissb  4894  disjor  5078  dftr2  5205  ssrelrel  5743  cotrg  6066  fununi  6565  dff13  7198  dffi2  9324  aceq2  10027  psgnunilem4  19424  metcld  25260  metcld2  25261  isch2  31247  disjorf  32603  funcnv5mpt  32695  bnj1052  35080  bnj1030  35092  dfon2lem8  35931  bj-ssbeq  36797  bj-ssbid2ALT  36807  bj-sblem1  36986  bj-sblem2  36987  bj-sblem  36988  wl-equsalvw  37682  ineleq  38486  cocossss  38638  cossssid3  38671  trcoss2  38686  elmapintrab  43759  elinintrab  43760  undmrnresiss  43787  elintima  43836  relexp0eq  43884  dfhe3  43958  ismnuprim  44477  pm10.52  44548  truniALT  44724  tpid3gVD  45024  truniALTVD  45060  onfrALTVD  45073  unisnALT  45108