Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcxfr GIF version

Theorem nfcxfr 2191
 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 2190 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 138 1 𝑥𝐴
 Colors of variables: wff set class Syntax hints:   = wceq 1259  Ⅎwnfc 2181 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-nf 1366  df-cleq 2049  df-clel 2052  df-nfc 2183 This theorem is referenced by:  nfrab1  2506  nfrabxy  2507  nfdif  3093  nfun  3127  nfin  3171  nfpw  3399  nfpr  3448  nfsn  3458  nfop  3593  nfuni  3614  nfint  3653  nfiunxy  3711  nfiinxy  3712  nfiunya  3713  nfiinya  3714  nfiu1  3715  nfii1  3716  nfopab  3853  nfopab1  3854  nfopab2  3855  nfmpt  3877  nfmpt1  3878  repizf2  3943  nfsuc  4173  nfxp  4399  nfco  4529  nfcnv  4542  nfdm  4606  nfrn  4607  nfres  4642  nfima  4704  nfiota1  4897  nffv  5213  fvmptss2  5275  fvmptssdm  5283  fvmptf  5291  ralrnmpt  5337  rexrnmpt  5338  f1ompt  5348  f1mpt  5438  fliftfun  5464  nfriota1  5503  riotaprop  5519  nfoprab1  5582  nfoprab2  5583  nfoprab3  5584  nfoprab  5585  nfmpt21  5599  nfmpt22  5600  nfmpt2  5601  ovmpt2s  5652  ov2gf  5653  ovi3  5665  nftpos  5925  nfrecs  5953  nffrec  6013  xpcomco  6331  nfsup  6398  caucvgprprlemaddq  6864  nfiseq  9382  nfsum1  10106  nfsum  10107
 Copyright terms: Public domain W3C validator