Theorem 19.23v 1969

Description: Version of 19.23 2253 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 1994. (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 1861	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1939	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 36	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1937	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 17	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1866	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 18	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 212	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  19.23vv  1970  pm11.53v  1971  equsv  2030  sb4b  2513  2mo2  2681  ceqsalv  3502  clel2g  3627  clel4g  3631  elabd2  3638  elabgt  3640  elabgtOLD  3641  euind  3696  reuind  3725  sbcg  3825  ralsng  4646  snssb  4753  unissb  4910  disjor  5095  dftr2  5224  ssrelrel  5783  cotrg  6112  fununi  6612  dff13  7253  dffi2  9382  aceq2  10102  psgnunilem4  19566  metcld  25433  metcld2  25434  isch2  31515  disjorf  32864  funcnv5mpt  32952  bnj1052  35307  bnj1030  35319  dfon2lem8  36178  mh-unprimbi  36943  mh-infprim1bi  36945  bj-ssbeq  37163  bj-ssbid2ALT  37173  bj-sblem1  37365  bj-sblem2  37366  bj-sblem  37367  wl-equsalvw  38080  ineleq  38892  cocossss  39064  cossssid3  39097  trcoss2  39112  elmapintrab  44193  elinintrab  44194  undmrnresiss  44221  elintima  44270  relexp0eq  44318  dfhe3  44392  ismnuprim  44895  pm10.52  44966  truniALT  45141  tpid3gVD  45441  truniALTVD  45477  onfrALTVD  45490  unisnALT  45525