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 sb8f ⊢ ∀ z Ⅎ x z ∈ A ↔ ∀ y y z Ⅎ x z ∈ A
6 sbnf ⊢ y z Ⅎ x z ∈ A ↔ Ⅎ x y z z ∈ A
7 clelsb1 ⊢ 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