Theorem nfcriOLDOLD

Description: Obsolete version of nfcri as of 26-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	nfcrii.1	⊢ Ⅎ 𝑥 𝐴
Assertion	nfcriOLDOLD	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfcrii.1	⊢ Ⅎ 𝑥 𝐴
2		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
3	2	nfbidv	⊢ ( 𝑧 = 𝑦 → ( Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐴 ) )
4		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
5	4	biimpi	⊢ ( Ⅎ 𝑥 𝐴 → ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
6		df-nf	⊢ ( Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
7	6	albii	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
8		sp	⊢ ( ∀ 𝑧 ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) → ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
9	7 8	sylbi	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 → ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
10	1 5 9	mp2b	⊢ ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 )
11	10	nfi	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
12	3 11	chvarvv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴