Theorem 19.21v 1868

Description: Version of 19.21 2075 with a dv condition, requiring fewer axioms.

Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as F/ x ph. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1710) instead of a dv condition. For instance, 19.21v 1868 versus 19.21 2075 and vtoclf 3258 versus vtocl 3259. Note that "not free in" is less restrictive than "does not occur in." Note that the version with a dv condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1843. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.)

Assertion

Ref	Expression
19.21v	|- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem 19.21v

Step	Hyp	Ref	Expression
1		stdpc5v 1867	. 2 |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
2		ax5e 1841	. . . 4 |- ( E. x ph -> ph )
3	2	imim1i 63	. . 3 |- ( ( ph -> A. x ps ) -> ( E. x ph -> A. x ps ) )
4		19.38 1766	. . 3 |- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
5	3, 4	syl 17	. 2 |- ( ( ph -> A. x ps ) -> A. x ( ph -> ps ) )
6	1, 5	impbii 199	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  19.32v  1869  pm11.53v  1906  19.12vvv  1907  pm11.53  2179  19.12vv  2180  cbval2  2279  cbvaldva  2281  sbhb  2438  2sb6  2444  r2al  2939  r3al  2940  r19.21v  2960  ceqsralt  3229  rspc2gv  3321  euind  3393  reu2  3394  reuind  3411  unissb  4469  dfiin2g  4553  axrep5  4776  asymref  5512  fvn0ssdmfun  6350  dff13  6512  mpt22eqb  6769  findcard3  8203  marypha1lem  8339  marypha2lem3  8343  aceq1  8940  kmlem15  8986  cotr2g  13715  bnj864  30992  bnj865  30993  bnj978  31019  bnj1176  31073  bnj1186  31075  dfon2lem8  31695  dffun10  32021  bj-ssb1  32633  bj-ssbcom3lem  32650  bj-cbval2v  32737  bj-axrep5  32792  bj-ralcom4  32868  mpt2bi123f  33971  mptbi12f  33975  elmapintrab  37882  undmrnresiss  37910  dfhe3  38069  dffrege115  38272  ntrneiiso  38389  ntrneikb  38392  pm10.541  38566  pm10.542  38567  19.21vv  38575  pm11.62  38594  2sbc6g  38616  2rexsb  41170