MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21v Structured version   Unicode version

Theorem 19.21v 1909
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/ x ph in 19.21 1839 via the use of distinct variable conditions combined with nfv 1673. 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 2263 derived from df-eu 2257. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 21-Jun-1993.)
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
StepHypRef Expression
1 nfv 1673 . 2  |-  F/ x ph
2119.21 1839 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590
This theorem is referenced by:  pm11.53  1912  19.12vv  1917  cbval2  1975  sbhb  2143  2sb6  2150  sbcom2OLD  2152  2sb6rfOLD  2162  2exsbOLD  2183  r3al  2773  ceqsralt  2996  euind  3146  reu2  3147  reuind  3162  unissb  4123  dfiin2g  4203  axrep5  4408  asymref  5214  dff13  5971  mpt22eqb  6199  findcard3  7555  marypha1lem  7683  marypha2lem3  7687  aceq1  8287  kmlem15  8333  dfon2lem8  27603  dffun10  27945  mpt2bi123f  28975  mptbi12f  28979  pm10.541  29619  pm10.542  29620  19.21vv  29628  pm11.62  29647  2sbc6g  29669  2rexsb  29994  bnj864  31915  bnj865  31916  bnj978  31942  bnj1176  31996  bnj1186  31998  bj-cbval2v  32238  bj-axrep5  32313  bj-ralcom4  32379
  Copyright terms: Public domain W3C validator