Theorem 19.23v 1944

Description: Version of 19.23 2219 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 1969. (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 1836	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1914	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1912	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1841	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  19.23vv  1945  pm11.53v  1946  equsv  2005  sb4b  2480  2mo2  2648  ceqsalv  3470  clel2g  3602  clel4g  3606  elabd2  3613  elabgt  3615  elabgtOLD  3616  elabgtOLDOLD  3617  euind  3671  reuind  3700  sbcg  3802  ralsng  4620  snssb  4727  unissb  4884  disjor  5068  dftr2  5195  ssrelrel  5746  cotrg  6069  fununi  6568  dff13  7203  dffi2  9330  aceq2  10035  psgnunilem4  19466  metcld  25286  metcld2  25287  isch2  31312  disjorf  32667  funcnv5mpt  32758  bnj1052  35136  bnj1030  35148  dfon2lem8  35989  mh-unprimbi  36745  mh-infprim1bi  36747  bj-ssbeq  36966  bj-ssbid2ALT  36976  bj-sblem1  37168  bj-sblem2  37169  bj-sblem  37170  wl-equsalvw  37880  ineleq  38692  cocossss  38864  cossssid3  38897  trcoss2  38912  elmapintrab  44024  elinintrab  44025  undmrnresiss  44052  elintima  44101  relexp0eq  44149  dfhe3  44223  ismnuprim  44742  pm10.52  44813  truniALT  44989  tpid3gVD  45289  truniALTVD  45325  onfrALTVD  45338  unisnALT  45373