Theorem 19.23v 1939

Description: Version of 19.23 2207 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 1966. (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 1830	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1909	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1907	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1835	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 211	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  19.23vv  1940  pm11.53v  1941  equsv  2005  sbequ2OLD  2247  sb4b  2495  sb4bOLD  2496  2mo2  2728  euind  3714  reuind  3743  unissb  4862  disjor  5038  dftr2  5166  ssrelrel  5663  cotrg  5965  dffun2  6359  fununi  6423  dff13  7007  dffi2  8881  aceq2  9539  psgnunilem4  18619  metcld  23903  metcld2  23904  isch2  28994  disjorf  30323  funcnv5mpt  30407  bnj1052  32242  bnj1030  32254  dfon2lem8  33030  bj-ssbeq  33981  bj-ssbid2ALT  33991  bj-sblem1  34161  bj-sblem2  34162  bj-sblem  34163  wl-equsalvw  34772  ineleq  35602  cocossss  35675  cossssid3  35703  trcoss2  35718  elmapintrab  39929  elinintrab  39930  undmrnresiss  39957  elintima  39991  relexp0eq  40039  dfhe3  40114  ismnuprim  40623  pm10.52  40690  truniALT  40868  tpid3gVD  41169  truniALTVD  41205  onfrALTVD  41218  unisnALT  41253