Theorem eliin2f 42327

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

Hypothesis

Ref	Expression
eliin2f.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
eliin2f	⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem eliin2f

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliin 4909	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
2	1	adantl 485	. 2 ⊢ ((𝐵 ≠ ∅ ∧ 𝐴 ∈ V) → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
3		prcnel 3431	. . . 4 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)
4	3	adantl 485	. . 3 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ¬ 𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶)
5		n0 4261	. . . . . . . . 9 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
6	5	biimpi 219	. . . . . . . 8 ⊢ (𝐵 ≠ ∅ → ∃𝑦 𝑦 ∈ 𝐵)
7	6	adantr 484	. . . . . . 7 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦 𝑦 ∈ 𝐵)
8		prcnel 3431	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)
9	8	a1d 25	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
10	9	adantl 485	. . . . . . . . 9 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝑦 ∈ 𝐵 → ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
11	10	ancld 554	. . . . . . . 8 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
12	11	eximdv 1925	. . . . . . 7 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (∃𝑦 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)))
13	7, 12	mpd 15	. . . . . 6 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
14		df-rex 3067	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
15	13, 14	sylibr 237	. . . . 5 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)
16		eliin2f.1	. . . . . 6 ⊢ Ⅎ𝑥𝐵
17		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑦𝐵
18		nfv 1922	. . . . . 6 ⊢ Ⅎ𝑦 ¬ 𝐴 ∈ 𝐶
19		nfcsb1v 3836	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶
20	19	nfel2 2922	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶
21	20	nfn 1865	. . . . . 6 ⊢ Ⅎ𝑥 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶
22		csbeq1a 3825	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶)
23	22	eleq2d 2823	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
24	23	notbid 321	. . . . . 6 ⊢ (𝑥 = 𝑦 → (¬ 𝐴 ∈ 𝐶 ↔ ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶))
25	16, 17, 18, 21, 24	cbvrexfw 3346	. . . . 5 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 ¬ 𝐴 ∈ ⦋𝑦 / 𝑥⦌𝐶)
26	15, 25	sylibr 237	. . . 4 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ∃𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶)
27		rexnal 3160	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝐴 ∈ 𝐶 ↔ ¬ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
28	26, 27	sylib 221	. . 3 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → ¬ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)
29	4, 28	2falsed 380	. 2 ⊢ ((𝐵 ≠ ∅ ∧ ¬ 𝐴 ∈ V) → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
30	2, 29	pm2.61dan 813	1 ⊢ (𝐵 ≠ ∅ → (𝐴 ∈ ∩ 𝑥 ∈ 𝐵 𝐶 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∃wex 1787   ∈ wcel 2110  Ⅎwnfc 2884   ≠ wne 2940  ∀wral 3061  ∃wrex 3062  Vcvv 3408  ⦋csb 3811  ∅c0 4237  ∩ ciin 4905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-nul 4238  df-iin 4907

This theorem is referenced by:  eliin2  42338