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

Theorem nfcxfr 2217
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  |-  A  =  B
nfcxfr.2  |-  F/_ x B
Assertion
Ref Expression
nfcxfr  |-  F/_ x A

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2  |-  F/_ x B
2 nfceqi.1 . . 3  |-  A  =  B
32nfceqi 2216 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 144 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1285   F/_wnfc 2207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-cleq 2075  df-clel 2078  df-nfc 2209
This theorem is referenced by:  nfrab1  2534  nfrabxy  2535  nfdif  3094  nfun  3129  nfin  3179  nfpw  3402  nfpr  3450  nfsn  3460  nfop  3594  nfuni  3615  nfint  3654  nfiunxy  3712  nfiinxy  3713  nfiunya  3714  nfiinya  3715  nfiu1  3716  nfii1  3717  nfopab  3854  nfopab1  3855  nfopab2  3856  nfmpt  3878  nfmpt1  3879  repizf2  3944  nfsuc  4171  nfxp  4397  nfco  4529  nfcnv  4542  nfdm  4606  nfrn  4607  nfres  4642  nfima  4706  nfiota1  4899  nffv  5216  fvmptss2  5279  fvmptssdm  5287  fvmptf  5295  ralrnmpt  5341  rexrnmpt  5342  f1ompt  5352  f1mpt  5442  fliftfun  5467  nfriota1  5506  riotaprop  5522  nfoprab1  5585  nfoprab2  5586  nfoprab3  5587  nfoprab  5588  nfmpt21  5602  nfmpt22  5603  nfmpt2  5604  ovmpt2s  5655  ov2gf  5656  ovi3  5668  nftpos  5928  nfrecs  5956  nffrec  6045  xpcomco  6370  nfsup  6464  nfinf  6489  caucvgprprlemaddq  6960  nfiseq  9528  nfsum1  10331  nfsum  10332
  Copyright terms: Public domain W3C validator