Theorem 19.23v 1975

Description: Version of 19.23 2250 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 2000. (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 1945	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1943	. . . 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 1943

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

This theorem is used by:  19.23vv  1976  pm11.53v  1977  equsv  2036  sb4b  2509  2mo2  2677  ceqsalv  3496  clel2g  3620  clel4g  3624  elabd2  3631  elabgt  3633  elabgtOLD  3634  euind  3689  reuind  3718  sbcg  3818  ralsng  4643  snssb  4750  unissb  4908  disjor  5093  dftr2  5222  ssrelrel  5784  cotrg  6113  fununi  6615  dff13  7257  dffi2  9390  aceq2  10119  psgnunilem4  19611  metcld  25516  metcld2  25517  isch2  31646  disjorf  32995  funcnv5mpt  33083  bnj1052  35428  bnj1030  35440  dfon2lem8  36317  mh-unprimbi  37112  mh-infprim1bi  37114  bj-ssbeq  37332  bj-ssbid2ALT  37342  bj-sblem1  37534  bj-sblem2  37535  bj-sblem  37536  wl-equsalvw  38250  ineleq  39061  cocossss  39233  cossssid3  39266  trcoss2  39281  elmapintrab  44360  elinintrab  44361  undmrnresiss  44388  elintima  44437  relexp0eq  44485  dfhe3  44559  ismnuprim  45062  pm10.52  45133  truniALT  45308  tpid3gVD  45608  truniALTVD  45644  onfrALTVD  45657  unisnALT  45692