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

Theorem 19.21v 1930
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 1853 via the use of distinct variable conditions, often combined with nfv 1683. 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 2285 derived from df-eu 2279. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-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
StepHypRef Expression
1 ax-5 1680 . . 3  |-  ( ph  ->  A. x ph )
2 alim 1613 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
31, 2syl5 32 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  A. x ps )
)
4 ax5e 1682 . . . 4  |-  ( E. x ph  ->  ph )
54imim1i 58 . . 3  |-  ( (
ph  ->  A. x ps )  ->  ( E. x ph  ->  A. x ps )
)
6 19.38 1639 . . 3  |-  ( ( E. x ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
75, 6syl 16 . 2  |-  ( (
ph  ->  A. x ps )  ->  A. x ( ph  ->  ps ) )
83, 7impbii 188 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  pm11.53  1937  19.12vv  1942  cbval2  2000  sbhb  2165  2sb6  2172  sbcom2OLD  2174  2sb6rfOLD  2184  2exsbOLD  2205  r2al  2845  r3al  2847  r19.21v  2872  r3alOLD  2905  ceqsralt  3142  euind  3295  reu2  3296  reuind  3312  unissb  4283  dfiin2g  4364  axrep5  4569  asymref  5389  fvn0ssdmfun  6023  dff13  6165  mpt22eqb  6406  findcard3  7775  marypha1lem  7905  marypha2lem3  7909  aceq1  8510  kmlem15  8556  dfon2lem8  29149  dffun10  29491  mpt2bi123f  30499  mptbi12f  30503  pm10.541  31174  pm10.542  31175  19.21vv  31183  pm11.62  31202  2sbc6g  31224  2rexsb  31965  bnj864  33460  bnj865  33461  bnj978  33487  bnj1176  33541  bnj1186  33543  bj-cbval2v  33785  bj-axrep5  33860  bj-ralcom4  33926
  Copyright terms: Public domain W3C validator