Theorem 19.23v 1889

Description: Version of 19.23 2067 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)

Assertion

Ref	Expression
19.23v	⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		exim 1751	. . 3 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		19.9v 1883	. . 3 ⊢ (∃𝑥𝜓 ↔ 𝜓)
3	1, 2	syl6ib 240	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜓))
4		ax-5 1827	. . . 4 ⊢ (𝜓 → ∀𝑥𝜓)
5	4	imim2i 16	. . 3 ⊢ ((∃𝑥𝜑 → 𝜓) → (∃𝑥𝜑 → ∀𝑥𝜓))
6		19.38 1757	. . 3 ⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
7	5, 6	syl 17	. 2 ⊢ ((∃𝑥𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
8	3, 7	impbii 198	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  19.23vv  1890  pm11.53v  1893  equsalvw  1918  2mo2  2538  euind  3360  reuind  3378  unissb  4405  disjor  4567  dftr2  4682  ssrelrel  5143  cotrg  5426  dffun2  5814  fununi  5878  dff13  6416  dffi2  8212  aceq2  8825  psgnunilem4  17740  metcld  22912  metcld2  22913  isch2  27464  disjorf  28774  funcnv5mpt  28852  bnj1052  30297  bnj1030  30309  dfon2lem8  30939  bj-ssbeq  31816  bj-ssb0  31817  bj-ssb1a  31821  bj-ssb1  31822  bj-ssbequ2  31832  bj-ssbid2ALT  31835  elmapintrab  36901  elinintrab  36902  undmrnresiss  36929  elintima  36964  relexp0eq  37012  dfhe3  37089  pm10.52  37586  truniALT  37772  tpid3gVD  38099  truniALTVD  38136  onfrALTVD  38149  unisnALT  38184