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

Theorem 19.21 1814
 Description: Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
19.21.1
Assertion
Ref Expression
19.21

Proof of Theorem 19.21
StepHypRef Expression
1 19.21.1 . 2
2 19.21t 1813 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1549  wnf 1553 This theorem is referenced by:  19.21h  1815  stdpc5  1816  nfim1OLD  1831  19.21-2  1887  nf3  1890  19.32  1896  19.21v  1913  19.12vv  1921  cbv1  1973  ax15  2107  eu2  2306  moanim  2337  r2alf  2740  19.12b  25429  ax15NEW7  29536  19.12vvOLD7  29701 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator