Theorem 19.23v 1942

Description: Version of 19.23 2212 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 1834	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		ax5e 1912	. . 3 ⊢ (∃𝑥𝜓 → 𝜓)
3	1, 2	syl6 35	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1910	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1839	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 209	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  19.23vv  1943  pm11.53v  1944  equsv  2003  sb4b  2473  2mo2  2640  ceqsalv  3476  clel2g  3614  clel4g  3618  elabd2  3625  elabgt  3627  elabgtOLD  3628  elabgtOLDOLD  3629  euind  3684  reuind  3713  sbcg  3815  ralsng  4627  snssb  4734  unissb  4890  disjor  5074  dftr2  5201  ssrelrel  5739  cotrg  6060  fununi  6557  dff13  7191  dffi2  9313  aceq2  10013  psgnunilem4  19376  metcld  25204  metcld2  25205  isch2  31167  disjorf  32523  funcnv5mpt  32611  bnj1052  34942  bnj1030  34954  dfon2lem8  35764  bj-ssbeq  36627  bj-ssbid2ALT  36637  bj-sblem1  36816  bj-sblem2  36817  bj-sblem  36818  wl-equsalvw  37512  ineleq  38322  cocossss  38413  cossssid3  38446  trcoss2  38461  elmapintrab  43549  elinintrab  43550  undmrnresiss  43577  elintima  43626  relexp0eq  43674  dfhe3  43748  ismnuprim  44267  pm10.52  44338  truniALT  44515  tpid3gVD  44815  truniALTVD  44851  onfrALTVD  44864  unisnALT  44899