Theorem nfcriiOLD

Description: Obsolete version of nfcrii as of 23-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nfcriOLD.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfcriiOLD	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfcriOLD.1	⊢ Ⅎ 𝑥 𝐴
2	1	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
3	2	nfsbv	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴
4	3	nf5ri	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 → ∀ 𝑥 [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 )
5		clelsb1	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
6	5	albii	⊢ ( ∀ 𝑥 [ 𝑦 / 𝑧 ] 𝑧 ∈ 𝐴 ↔ ∀ 𝑥 𝑦 ∈ 𝐴 )
7	4 5 6	3imtr3i	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )