Theorem nfcjust

Description: Justification theorem for df-nfc . (Contributed by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Assertion	nfcjust	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eleq1w	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
2	1	nfbidv	⊢ ( 𝑦 = 𝑧 → ( Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑧 ∈ 𝐴 ) )
3	2	cbvalvw	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )