Theorem 19.23v 1962

Description: Version of 19.23 2246 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 1987. (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 1854	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1932	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1930	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1859	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 211	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  19.23vv  1963  pm11.53v  1964  equsv  2023  sb4b  2506  2mo2  2674  ceqsalv  3493  clel2g  3618  clel4g  3622  elabd2  3629  elabgt  3631  elabgtOLD  3632  euind  3687  reuind  3716  sbcg  3816  ralsng  4634  snssb  4741  unissb  4899  disjor  5082  dftr2  5209  ssrelrel  5768  cotrg  6098  fununi  6596  dff13  7238  dffi2  9369  aceq2  10075  psgnunilem4  19537  metcld  25365  metcld2  25366  isch2  31423  disjorf  32776  funcnv5mpt  32866  bnj1052  35267  bnj1030  35279  dfon2lem8  36135  mh-unprimbi  36901  mh-infprim1bi  36903  bj-ssbeq  37122  bj-ssbid2ALT  37132  bj-sblem1  37324  bj-sblem2  37325  bj-sblem  37326  wl-equsalvw  38038  ineleq  38850  cocossss  39022  cossssid3  39055  trcoss2  39070  elmapintrab  44149  elinintrab  44150  undmrnresiss  44177  elintima  44226  relexp0eq  44274  dfhe3  44348  ismnuprim  44867  pm10.52  44938  truniALT  45114  tpid3gVD  45414  truniALTVD  45450  onfrALTVD  45463  unisnALT  45498