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

Theorem 19.21 1815
 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 1814 . 2
31, 2ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178  wal 1550  wnf 1554 This theorem is referenced by:  19.21h  1816  stdpc5  1817  nfim1OLD  1832  19.21-2  1888  nf3  1891  19.32  1897  19.21v  1914  19.12vv  1922  cbv1  1974  ax15  2109  eu2  2308  moanim  2339  r2alf  2742  19.12b  25434  ax15NEW7  29610  19.12vvOLD7  29775 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator