New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfcxfr Unicode version

Theorem nfcxfr 2486
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfceqi.1
nfcxfr.2
Assertion
Ref Expression
nfcxfr

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2
2 nfceqi.1 . . 3
32nfceqi 2485 . 2
41, 3mpbir 200 1
 Colors of variables: wff setvar class Syntax hints:   wceq 1642  wnfc 2476 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-cleq 2346  df-clel 2349  df-nfc 2478 This theorem is referenced by:  nfrab1  2791  nfrab  2792  nfnin  3228  nfcompl  3229  nfin  3230  nfun  3231  nfdif  3232  nfsymdif  3233  nfpw  3733  nfpr  3773  nfsn  3784  nfuni  3897  nfint  3936  nfiun  3995  nfiin  3996  nfiu1  3997  nfii1  3998  nfopk  4068  nfiota1  4341  nfop  4604  nfopab  4627  nfopab1  4628  nfopab2  4629  nfxp  4810  nfco  4882  nfcnv  4891  nfres  4936  nfima  4953  nfrn  4963  nfdm  4964  nffv  5334  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548  nfoprab  5549  ov3  5599  nfmpt  5671  nfmpt1  5672  nfmpt21  5673  nfmpt22  5674  nfmpt2  5675  fvmptss  5705  ov2gf  5711  fvmptf  5722
 Copyright terms: Public domain W3C validator