Theorem 19.23v 1977

Description: Version of 19.23 2251 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 2002. (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 1867	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1947	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1945	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 17	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1872	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 18	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  19.23vv  1978  pm11.53v  1979  equsv  2038  sb4b  2507  2mo2  2675  ceqsalv  3493  clel2g  3616  clel4g  3620  elabd2  3627  elabgt  3629  elabgtOLD  3630  euind  3685  reuind  3714  sbcg  3814  ralsng  4637  snssb  4745  unissb  4906  disjor  5090  dftr2  5220  ssrelrel  5781  cotrg  6123  fununi  6645  dff13  7289  dffi2  9452  aceq2  10237  psgnunilem4  19762  metcld  25682  metcld2  25683  isch2  31882  disjorf  33271  funcnv5mpt  33359  bnj1052  35716  bnj1030  35728  dfon2lem8  36767  mh-unprimbi  37547  mh-infprim1bi  37549  bj-ssbeq  37767  bj-ssbid2ALT  37777  bj-sblem1  37969  bj-sblem2  37970  bj-sblem  37971  wl-equsalvw  38738  ineleq  39552  cocossss  39724  cossssid3  39757  trcoss2  39772  elmapintrab  44838  elinintrab  44839  undmrnresiss  44865  elintima  44914  relexp0eq  44962  dfhe3  45036  ismnuprim  45539  pm10.52  45610  truniALT  45784  tpid3gVD  46084  truniALTVD  46120  onfrALTVD  46133  unisnALT  46168