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