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 𝑦 𝐴
Assertion bj-nfcf ( 𝑥 𝐴 ↔ ∀ 𝑦𝑥 𝑦𝐴 )

Proof

Step Hyp Ref Expression
1 bj-nfcf.nf 𝑦 𝐴
2 df-nfc ( 𝑥 𝐴 ↔ ∀ 𝑧𝑥 𝑧𝐴 )
3 1 nfcri 𝑦 𝑧𝐴
4 3 nfnf 𝑦𝑥 𝑧𝐴
5 4 sb8v ( ∀ 𝑧𝑥 𝑧𝐴 ↔ ∀ 𝑦 [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧𝐴 )
6 bj-sbnf ( [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧𝐴 ↔ Ⅎ 𝑥 [ 𝑦 / 𝑧 ] 𝑧𝐴 )
7 clelsb3 ( [ 𝑦 / 𝑧 ] 𝑧𝐴𝑦𝐴 )
8 7 nfbii ( Ⅎ 𝑥 [ 𝑦 / 𝑧 ] 𝑧𝐴 ↔ Ⅎ 𝑥 𝑦𝐴 )
9 6 8 bitri ( [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧𝐴 ↔ Ⅎ 𝑥 𝑦𝐴 )
10 9 albii ( ∀ 𝑦 [ 𝑦 / 𝑧 ] Ⅎ 𝑥 𝑧𝐴 ↔ ∀ 𝑦𝑥 𝑦𝐴 )
11 5 10 bitri ( ∀ 𝑧𝑥 𝑧𝐴 ↔ ∀ 𝑦𝑥 𝑦𝐴 )
12 2 11 bitri ( 𝑥 𝐴 ↔ ∀ 𝑦𝑥 𝑦𝐴 )