Theorem nfcri 2484

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

Hypothesis

Ref	Expression
nfcri.1	|- F/_xA

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/_xA
2	1	nfcrii 2483	. 2 |- (y e. A -> A.x y e. A)
3	2	nfi 1551	1 |- F/x y e. A

Syntax hints:   F/wnf 1544   e. wcel 1710   F/_wnfc 2477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2479

This theorem is referenced by:  nfnfc  2496  nfeq  2497  nfel  2498  cleqf  2514  sbabel  2516  r2alf  2650  r2exf  2651  nfrab  2793  cbvralf  2830  cbvrab  2858  sbcabel  3124  cbvcsb  3141  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  dfss2f  3265  nfiun  3996  nfiin  3997  cbviun  4004  cbviin  4005  nfxp  4811  opeliunxp  4821  nfmpt  5672  nfmpt2  5676  cbvmpt2x  5679  fmpt2x  5731