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

Theorem nfcxfr 2222
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 2221 . 2  |-  ( F/_ x A  <->  F/_ x B )
41, 3mpbir 144 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    = wceq 1287   F/_wnfc 2212
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-cleq 2078  df-clel 2081  df-nfc 2214
This theorem is referenced by:  nfrab1  2542  nfrabxy  2543  nfdif  3110  nfun  3145  nfin  3195  nfpw  3426  nfpr  3474  nfsn  3484  nfop  3620  nfuni  3641  nfint  3680  nfiunxy  3738  nfiinxy  3739  nfiunya  3740  nfiinya  3741  nfiu1  3742  nfii1  3743  nfopab  3880  nfopab1  3881  nfopab2  3882  nfmpt  3904  nfmpt1  3905  repizf2  3970  nfsuc  4207  nfxp  4435  nfco  4567  nfcnv  4581  nfdm  4645  nfrn  4646  nfres  4681  nfima  4745  nfiota1  4944  nffv  5271  fvmptss2  5335  fvmptssdm  5343  fvmptf  5351  ralrnmpt  5397  rexrnmpt  5398  f1ompt  5406  f1mpt  5504  fliftfun  5529  nfriota1  5569  riotaprop  5585  nfoprab1  5648  nfoprab2  5649  nfoprab3  5650  nfoprab  5651  nfmpt21  5665  nfmpt22  5666  nfmpt2  5667  ovmpt2s  5718  ov2gf  5719  ovi3  5731  nfof  5811  nfofr  5812  nftpos  5991  nfrecs  6019  nffrec  6108  xpcomco  6487  nfsup  6623  nfinf  6648  nfdju  6671  caucvgprprlemaddq  7203  nfiseq  9778  nfsum1  10627  nfsum  10628
  Copyright terms: Public domain W3C validator