Theorem nfcri 2214

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2212, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfcri.1	|- F/_ x A

Assertion

Ref	Expression
nfcri	|- F/ x y e. A

Distinct variable group:   x, y

Allowed substitution hints:   A( x, y)

Proof of Theorem nfcri

Step	Hyp	Ref	Expression
1		nfcri.1	. . 3 |- F/_ x A
2	1	nfcrii 2213	. 2 |- ( y e. A -> A. x y e. A )
3	2	nfi 1392	1 |- F/ x y e. A

Syntax hints:   F/wnf 1390   e. wcel 1434   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-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-cleq 2075  df-clel 2078  df-nfc 2209

This theorem is referenced by:  nfnfc  2226  nfeq  2227  nfel  2228  cleqf  2243  sbabel  2245  r2alf  2384  r2exf  2385  nfrabxy  2535  cbvralf  2572  cbvrexf  2573  cbvrab  2600  nfccdeq  2814  sbcabel  2896  cbvcsb  2913  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  dfss2f  2991  nfdif  3094  nfun  3129  nfin  3179  nfop  3594  nfiunxy  3712  nfiinxy  3713  nfiunya  3714  nfiinya  3715  cbviun  3723  cbviin  3724  cbvdisj  3784  nfdisjv  3786  nfmpt  3878  nffrfor  4111  onintrab2im  4270  tfis  4332  nfxp  4397  opeliunxp  4421  iunxpf  4512  elrnmpt1  4613  fvmptssdm  5287  nfmpt2  5604  cbvmpt2x  5613  fmpt2x  5857  nffrec  6045  nfsum1  10331  nfsum  10332