Theorem 19.23v 1975

Description: Version of 19.23 2248 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  2505  2mo2  2673  ceqsalv  3490  clel2g  3613  clel4g  3617  elabd2  3624  elabgt  3626  elabgtOLD  3627  euind  3682  reuind  3711  sbcg  3811  ralsng  4636  snssb  4743  unissb  4901  disjor  5085  dftr2  5214  ssrelrel  5772  cotrg  6105  fununi  6613  dff13  7256  dffi2  9408  aceq2  10191  psgnunilem4  19704  metcld  25620  metcld2  25621  isch2  31818  disjorf  33166  funcnv5mpt  33254  bnj1052  35598  bnj1030  35610  dfon2lem8  36532  mh-unprimbi  37312  mh-infprim1bi  37314  bj-ssbeq  37532  bj-ssbid2ALT  37542  bj-sblem1  37734  bj-sblem2  37735  bj-sblem  37736  wl-equsalvw  38450  ineleq  39266  cocossss  39438  cossssid3  39471  trcoss2  39486  elmapintrab  44561  elinintrab  44562  undmrnresiss  44589  elintima  44638  relexp0eq  44686  dfhe3  44760  ismnuprim  45263  pm10.52  45334  truniALT  45509  tpid3gVD  45809  truniALTVD  45845  onfrALTVD  45858  unisnALT  45893