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 32607

Description: Append an element to a disjoint collection. Similar to ralunsn 4894, gsumunsn 19978, 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 5126	. . . . . 6 ⊢ (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
2		eqeq1 2741	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑀 = 𝑗))
3		csbeq1 3902	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑀 → ⦋𝑖 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
4	3	ineq1d 4219	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵))
5	4	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
6	2, 5	orbi12d 919	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
7	6	ralbidv 3178	. . . . . . 7 ⊢ (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
8	7	ralunsn 4894	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
9	1, 8	bitrid 283	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
10		eqeq2 2749	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑖 = 𝑀))
11		csbeq1 3902	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑀 → ⦋𝑗 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
12	11	ineq2d 4220	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
13	12	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
14	10, 13	orbi12d 919	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
15	14	ralunsn 4894	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
16	15	ralbidv 3178	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
17		eqeq2 2749	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑀 = 𝑗 ↔ 𝑀 = 𝑀))
18	11	ineq2d 4220	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
19	18	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
20	17, 19	orbi12d 919	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
21	20	ralunsn 4894	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
22		eqid 2737	. . . . . . . . 9 ⊢ 𝑀 = 𝑀
23	22	orci 866	. . . . . . . 8 ⊢ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)
24	23	biantru 529	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
25	21, 24	bitr4di 289	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
26	16, 25	anbi12d 632	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ((∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
27	9, 26	bitrd 279	. . . 4 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
28		r19.26 3111	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
29		disjors 5126	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
30	29	anbi1i 624	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
31	28, 30	bitr4i 278	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
32	31	anbi1i 624	. . . 4 ⊢ ((∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
33	27, 32	bitrdi 287	. . 3 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
34	33	adantr 480	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
35		orcom 871	. . . . . . . . 9 ⊢ (((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
36	35	ralbii 3093	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
37		r19.30 3120	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
38		risset 3233	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)
39		biorf 937	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
40	38, 39	sylnbi 330	. . . . . . . . . . 11 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
41	40	adantl 481	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
42		orcom 871	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
43	41, 42	bitrdi 287	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)))
44	37, 43	imbitrrid 246	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
45	36, 44	biimtrrid 243	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
46		olc 869	. . . . . . . 8 ⊢ ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
47	46	ralimi 3083	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
48	45, 47	impbid1 225	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
49		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝐵 ∩ 𝐶) = ∅
50		nfcsb1v 3923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
51		nfcv 2905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
52	50, 51	nfin 4224	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶)
53	52	nfeq1 2921	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
54		csbeq1a 3913	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
55	54	ineq1d 4219	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝐵 ∩ 𝐶) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
56	55	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
57	49, 53, 56	cbvralw 3306	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
58	57	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
59		ss0b 4401	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
60		iunss 5045	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
61		iunin1 5072	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
62	61	eqeq1i 2742	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
63	59, 60, 62	3bitr3ri 302	. . . . . . . . . 10 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
64		ss0b 4401	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ 𝐶) ⊆ ∅ ↔ (𝐵 ∩ 𝐶) = ∅)
65	64	ralbii 3093	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
66	63, 65	bitri 275	. . . . . . . . 9 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
67	66	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅))
68		nfcvd 2906	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑥𝐶)
69		disjunsn.s	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)
70	68, 69	csbiegf 3932	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑥⦌𝐵 = 𝐶)
71	70	ineq2d 4220	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
72	71	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
73	72	ralbidv 3178	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
74	58, 67, 73	3bitr4d 311	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
75	74	adantr 480	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
76	48, 75	bitr4d 282	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
77	76	anbi2d 630	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
78		orcom 871	. . . . . . . 8 ⊢ (((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
79	78	ralbii 3093	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
80		r19.30 3120	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
81		clel5 3665	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)
82		biorf 937	. . . . . . . . . . 11 ⊢ (¬ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
83	81, 82	sylnbi 330	. . . . . . . . . 10 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
84	83	adantl 481	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
85		orcom 871	. . . . . . . . 9 ⊢ ((∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
86	84, 85	bitrdi 287	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)))
87	80, 86	imbitrrid 246	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
88	79, 87	biimtrrid 243	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
89		olc 869	. . . . . . 7 ⊢ ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
90	89	ralimi 3083	. . . . . 6 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
91	88, 90	impbid1 225	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
92		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝐵 ∩ 𝐶) = ∅
93		nfcsb1v 3923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑗 / 𝑥⦌𝐵
94	93, 51	nfin 4224	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶)
95	94	nfeq1 2921	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
96		csbeq1a 3913	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑥⦌𝐵)
97	96	ineq1d 4219	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝐵 ∩ 𝐶) = (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶))
98	97	eqeq1d 2739	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
99	92, 95, 98	cbvralw 3306	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
100	99	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
101		incom 4209	. . . . . . . . . 10 ⊢ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵)
102	101	eqeq1i 2742	. . . . . . . . 9 ⊢ ((⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
103	102	ralbii 3093	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
104	100, 103	bitrdi 287	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
105	70	ineq1d 4219	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵))
106	105	eqeq1d 2739	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
107	106	ralbidv 3178	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
108	104, 67, 107	3bitr4d 311	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
109	108	adantr 480	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
110	91, 109	bitr4d 282	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
111	77, 110	anbi12d 632	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
112		anass 468	. . . 4 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
113		anidm 564	. . . . 5 ⊢ (((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
114	113	anbi2i 623	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
115	112, 114	bitri 275	. . 3 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
116	111, 115	bitrdi 287	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
117	34, 116	bitrd 279	1 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 ⦋csb 3899 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {csn 4626 ∪ ciun 4991 Disj wdisj 5110

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rmo 3380 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-sn 4627 df-iun 4993 df-disj 5111

This theorem is referenced by: disjun0 32608 disjiunel 32609

W3C validator