Theorem 19.23v 1975

Description: Version of 19.23 2247 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  2504  2mo2  2672  ceqsalv  3489  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  5776  cotrg  6105  fununi  6608  dff13  7251  dffi2  9393  aceq2  10122  psgnunilem4  19624  metcld  25534  metcld2  25535  isch2  31704  disjorf  33052  funcnv5mpt  33140  bnj1052  35484  bnj1030  35496  dfon2lem8  36367  mh-unprimbi  37163  mh-infprim1bi  37165  bj-ssbeq  37383  bj-ssbid2ALT  37393  bj-sblem1  37585  bj-sblem2  37586  bj-sblem  37587  wl-equsalvw  38301  ineleq  39102  cocossss  39274  cossssid3  39307  trcoss2  39322  elmapintrab  44416  elinintrab  44417  undmrnresiss  44444  elintima  44493  relexp0eq  44541  dfhe3  44615  ismnuprim  45118  pm10.52  45189  truniALT  45364  tpid3gVD  45664  truniALTVD  45700  onfrALTVD  45713  unisnALT  45748