Theorem nfcri 2483

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2481, 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 2482	. 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 2476

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 2478

This theorem is referenced by:  nfnfc  2495  nfeq  2496  nfel  2497  cleqf  2513  sbabel  2515  r2alf  2649  r2exf  2650  nfrab  2792  cbvralf  2829  cbvrab  2857  sbcabel  3123  cbvcsb  3140  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  dfss2f  3264  nfiun  3995  nfiin  3996  cbviun  4003  cbviin  4004  nfxp  4810  opeliunxp  4820  nfmpt  5671  nfmpt2  5675  cbvmpt2x  5678  fmpt2x  5730