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

Theorem nfrexd 2860
Description: Deduction version of nfrex 2861. (Contributed by Mario Carneiro, 14-Oct-2016.)
Hypotheses
Ref Expression
nfrexd.1  |-  F/ y
ph
nfrexd.2  |-  ( ph  -> 
F/_ x A )
nfrexd.3  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfrexd  |-  ( ph  ->  F/ x E. y  e.  A  ps )

Proof of Theorem nfrexd
StepHypRef Expression
1 dfrex2 2849 . 2  |-  ( E. y  e.  A  ps  <->  -. 
A. y  e.  A  -.  ps )
2 nfrexd.1 . . . 4  |-  F/ y
ph
3 nfrexd.2 . . . 4  |-  ( ph  -> 
F/_ x A )
4 nfrexd.3 . . . . 5  |-  ( ph  ->  F/ x ps )
54nfnd 1994 . . . 4  |-  ( ph  ->  F/ x  -.  ps )
62, 3, 5nfrald 2784 . . 3  |-  ( ph  ->  F/ x A. y  e.  A  -.  ps )
76nfnd 1994 . 2  |-  ( ph  ->  F/ x  -.  A. y  e.  A  -.  ps )
81, 7nfxfrd 1707 1  |-  ( ph  ->  F/ x E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   F/wnf 1677   F/_wnfc 2589   A.wral 2748   E.wrex 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754
This theorem is referenced by:  nfrex  2861  nfunid  4218
  Copyright terms: Public domain W3C validator