Theorem 19.23v 1941

Description: Version of 19.23 2199 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 1967. (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 1832	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1911	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1909	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1837	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 208	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1535  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 206  df-ex 1778

This theorem is referenced by:  19.23vv  1942  pm11.53v  1943  equsv  2002  sbequ2OLD  2237  sb4b  2470  sb4bOLD  2471  2mo2  2644  ceqsalv  3469  clel2g  3590  clel4g  3595  elabd2  3603  elabgt  3605  elabg  3609  euind  3661  reuind  3690  sbcg  3797  ralsng  4612  unissb  4876  disjor  5057  dftr2  5196  ssrelrel  5709  cotrg  6018  cotrgOLD  6019  dffun2OLD  6458  fununi  6526  dff13  7148  dffi2  9210  aceq2  9903  psgnunilem4  19133  metcld  24498  metcld2  24499  isch2  29613  disjorf  30946  funcnv5mpt  31033  bnj1052  32983  bnj1030  32995  dfon2lem8  33794  bj-ssbeq  34862  bj-ssbid2ALT  34872  bj-sblem1  35054  bj-sblem2  35055  bj-sblem  35056  wl-equsalvw  35725  ineleq  36512  cocossss  36585  cossssid3  36613  trcoss2  36628  elmapintrab  41208  elinintrab  41209  undmrnresiss  41236  elintima  41285  relexp0eq  41333  dfhe3  41407  ismnuprim  41936  pm10.52  42007  truniALT  42185  tpid3gVD  42486  truniALTVD  42522  onfrALTVD  42535  unisnALT  42570