New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nfcri | GIF version |
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.) |
Ref | Expression |
---|---|
nfcri.1 | ⊢ ℲxA |
Ref | Expression |
---|---|
nfcri | ⊢ Ⅎx y ∈ A |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcri.1 | . . 3 ⊢ ℲxA | |
2 | 1 | nfcrii 2482 | . 2 ⊢ (y ∈ A → ∀x y ∈ A) |
3 | 2 | nfi 1551 | 1 ⊢ Ⅎx y ∈ A |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1544 ∈ wcel 1710 Ⅎ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 |
Copyright terms: Public domain | W3C validator |