Theorem nfcriOLD

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

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

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		eleq1w	⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
9	8	exbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 𝑧 ∈ 𝐴 ↔ ∃ 𝑥 𝑤 ∈ 𝐴 ) )
10	8	albidv	⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑥 𝑧 ∈ 𝐴 ↔ ∀ 𝑥 𝑤 ∈ 𝐴 ) )
11	9 10	imbi12d	⊢ ( 𝑧 = 𝑤 → ( ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) ↔ ( ∃ 𝑥 𝑤 ∈ 𝐴 → ∀ 𝑥 𝑤 ∈ 𝐴 ) ) )
12	11	spw	⊢ ( ∀ 𝑧 ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) → ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
13	7 12	sylbi	⊢ ( ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 → ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 ) )
14	1 5 13	mp2b	⊢ ( ∃ 𝑥 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 )
15	14	nfi	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
16	3 15	chvarvv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴