disjunsn - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > disjunsn		Structured version Visualization version GIF version

Theorem disjunsn 30507

Description: Append an element to a disjoint collection. Similar to ralunsn 4782, gsumunsn 19199, etc. (Contributed by Thierry Arnoux, 28-Mar-2018.)

**Hypothesis**
Ref	Expression
disjunsn.s	⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)

**Assertion**
Ref	Expression
disjunsn	⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐶 𝑥,𝑀 𝑥,𝑉 Allowed substitution hint: 𝐵(𝑥)

Proof of Theorem disjunsn Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjors 5011	. . . . . 6 ⊢ (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
2		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑀 = 𝑗))
3		csbeq1 3793	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑀 → ⦋𝑖 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
4	3	ineq1d 4102	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵))
5	4	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
6	2, 5	orbi12d 918	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
7	6	ralbidv 3109	. . . . . . 7 ⊢ (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
8	7	ralunsn 4782	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
9	1, 8	syl5bb 286	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
10		eqeq2 2750	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑖 = 𝑀))
11		csbeq1 3793	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑀 → ⦋𝑗 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
12	11	ineq2d 4103	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
13	12	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
14	10, 13	orbi12d 918	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
15	14	ralunsn 4782	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
16	15	ralbidv 3109	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
17		eqeq2 2750	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑀 = 𝑗 ↔ 𝑀 = 𝑀))
18	11	ineq2d 4103	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
19	18	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
20	17, 19	orbi12d 918	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
21	20	ralunsn 4782	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
22		eqid 2738	. . . . . . . . 9 ⊢ 𝑀 = 𝑀
23	22	orci 864	. . . . . . . 8 ⊢ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)
24	23	biantru 533	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
25	21, 24	bitr4di 292	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
26	16, 25	anbi12d 634	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ((∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
27	9, 26	bitrd 282	. . . 4 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
28		r19.26 3084	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
29		disjors 5011	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
30	29	anbi1i 627	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
31	28, 30	bitr4i 281	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
32	31	anbi1i 627	. . . 4 ⊢ ((∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
33	27, 32	bitrdi 290	. . 3 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
34	33	adantr 484	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
35		orcom 869	. . . . . . . . 9 ⊢ (((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
36	35	ralbii 3080	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
37		r19.30 3244	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
38		risset 3177	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)
39		biorf 936	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
40	38, 39	sylnbi 333	. . . . . . . . . . 11 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
41	40	adantl 485	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
42		orcom 869	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
43	41, 42	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)))
44	37, 43	syl5ibr 249	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
45	36, 44	syl5bir 246	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
46		olc 867	. . . . . . . 8 ⊢ ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
47	46	ralimi 3075	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
48	45, 47	impbid1 228	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
49		nfv 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝐵 ∩ 𝐶) = ∅
50		nfcsb1v 3814	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
51		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
52	50, 51	nfin 4107	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶)
53	52	nfeq1 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
54		csbeq1a 3804	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
55	54	ineq1d 4102	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝐵 ∩ 𝐶) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
56	55	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
57	49, 53, 56	cbvralw 3340	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
58	57	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
59		ss0b 4286	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
60		iunss 4931	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
61		iunin1 4957	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
62	61	eqeq1i 2743	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
63	59, 60, 62	3bitr3ri 305	. . . . . . . . . 10 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
64		ss0b 4286	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ 𝐶) ⊆ ∅ ↔ (𝐵 ∩ 𝐶) = ∅)
65	64	ralbii 3080	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
66	63, 65	bitri 278	. . . . . . . . 9 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
67	66	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅))
68		nfcvd 2900	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑥𝐶)
69		disjunsn.s	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)
70	68, 69	csbiegf 3823	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑥⦌𝐵 = 𝐶)
71	70	ineq2d 4103	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
72	71	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
73	72	ralbidv 3109	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
74	58, 67, 73	3bitr4d 314	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
75	74	adantr 484	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
76	48, 75	bitr4d 285	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
77	76	anbi2d 632	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
78		orcom 869	. . . . . . . 8 ⊢ (((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
79	78	ralbii 3080	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
80		r19.30 3244	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
81		clel5 3563	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)
82		biorf 936	. . . . . . . . . . 11 ⊢ (¬ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
83	81, 82	sylnbi 333	. . . . . . . . . 10 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
84	83	adantl 485	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
85		orcom 869	. . . . . . . . 9 ⊢ ((∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
86	84, 85	bitrdi 290	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)))
87	80, 86	syl5ibr 249	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
88	79, 87	syl5bir 246	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
89		olc 867	. . . . . . 7 ⊢ ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
90	89	ralimi 3075	. . . . . 6 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
91	88, 90	impbid1 228	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
92		nfv 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝐵 ∩ 𝐶) = ∅
93		nfcsb1v 3814	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑗 / 𝑥⦌𝐵
94	93, 51	nfin 4107	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶)
95	94	nfeq1 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
96		csbeq1a 3804	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑥⦌𝐵)
97	96	ineq1d 4102	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝐵 ∩ 𝐶) = (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶))
98	97	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
99	92, 95, 98	cbvralw 3340	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
100	99	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
101		incom 4091	. . . . . . . . . 10 ⊢ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵)
102	101	eqeq1i 2743	. . . . . . . . 9 ⊢ ((⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
103	102	ralbii 3080	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
104	100, 103	bitrdi 290	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
105	70	ineq1d 4102	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵))
106	105	eqeq1d 2740	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
107	106	ralbidv 3109	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
108	104, 67, 107	3bitr4d 314	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
109	108	adantr 484	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
110	91, 109	bitr4d 285	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
111	77, 110	anbi12d 634	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
112		anass 472	. . . 4 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
113		anidm 568	. . . . 5 ⊢ (((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
114	113	anbi2i 626	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
115	112, 114	bitri 278	. . 3 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
116	111, 115	bitrdi 290	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
117	34, 116	bitrd 282	1 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 846 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ∃wrex 3054 ⦋csb 3790 ∪ cun 3841 ∩ cin 3842 ⊆ wss 3843 ∅c0 4211 {csn 4516 ∪ ciun 4881 Disj wdisj 4995

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-sn 4517 df-iun 4883 df-disj 4996

This theorem is referenced by: disjun0 30508 disjiunel 30509

W3C validator