Theorem eliin2f

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	eliin2f.1	⊢ Ⅎ 𝑥 𝐵
Assertion	eliin2f	⊢ ( 𝐵 ≠ ∅ → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eliin2f.1	⊢ Ⅎ 𝑥 𝐵
2		eliin	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
3	2	adantl	⊢ ( ( 𝐵 ≠ ∅ ∧ 𝐴 ∈ V ) → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
4		prcnel	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 )
5	4	adantl	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 )
6		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
7	6	birani	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑦 𝑦 ∈ 𝐵 )
8		prcnel	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
9	8	a1d	⊢ ( ¬ 𝐴 ∈ V → ( 𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
10	9	adantl	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ( 𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
11	10	ancld	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
12	11	eximdv	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
13	7 12	mpd	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
14		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
15	13 14	sylibr	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
16		nfcv	⊢ Ⅎ 𝑦 𝐵
17		nfv	⊢ Ⅎ 𝑦 ¬ 𝐴 ∈ 𝐶
18		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
19	18	nfel2	⊢ Ⅎ 𝑥 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶
20	19	nfn	⊢ Ⅎ 𝑥 ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶
21		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
22	21	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
23	22	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝐴 ∈ 𝐶 ↔ ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
24	1 16 17 20 23	cbvrexfw	⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
25	15 24	sylibr	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ∃ 𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶 )
26		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ¬ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )
27	25 26	sylib	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ¬ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 )
28	5 27	2falsed	⊢ ( ( 𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V ) → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )
29	3 28	pm2.61dan	⊢ ( 𝐵 ≠ ∅ → ( 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 ) )