Theorem 19.21v 1890

Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as F/xph in 19.21 1796 via the use of distinct variable conditions combined with nfv 1619. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2210 derived from df-eu 2208. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.)

Assertion

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

Distinct variable group:   ph,x

Allowed substitution hint:   ps(x)

Proof of Theorem 19.21v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/xph
2	1	19.21 1796	1 |- (A.x(ph -> ps) <-> (ph -> A.xps))

Syntax hints:   -> wi 4   <-> wb 176  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  pm11.53  1893  19.12vv  1898  sbhb  2107  2sb6  2113  sbcom2  2114  2sb6rf  2118  2exsb  2132  r3al  2672  ceqsralt  2883  euind  3024  reu2  3025  reuind  3040  unissb  3922  dfiin2g  4001  ssfin  4471  spfininduct  4541  dff13  5472  spacind  6288