Metamath Proof Explorer


Theorem bj-nfcf

Description: Version of df-nfc with a disjoint variable condition replaced with a nonfreeness hypothesis. (Contributed by BJ, 2-May-2019)

Ref Expression
Hypothesis bj-nfcf.nf _ y A
Assertion bj-nfcf _ x A y x y A

Proof

Step Hyp Ref Expression
1 bj-nfcf.nf _ y A
2 df-nfc _ x A z x z A
3 1 nfcri y z A
4 3 nfnf y x z A
5 4 sb8v z x z A y y z x z A
6 bj-sbnf y z x z A x y z z A
7 clelsb3 y z z A y A
8 7 nfbii x y z z A x y A
9 6 8 bitri y z x z A x y A
10 9 albii y y z x z A y x y A
11 5 10 bitri z x z A y x y A
12 2 11 bitri _ x A y x y A