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 32377

Description: Append an element to a disjoint collection. Similar to ralunsn 4890, gsumunsn 19908, 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 5123	. . . . . 6 ⊢ (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
2		eqeq1 2731	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑀 = 𝑗))
3		csbeq1 3892	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑀 → ⦋𝑖 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
4	3	ineq1d 4207	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵))
5	4	eqeq1d 2729	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
6	2, 5	orbi12d 917	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
7	6	ralbidv 3172	. . . . . . 7 ⊢ (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
8	7	ralunsn 4890	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
9	1, 8	bitrid 283	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
10		eqeq2 2739	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑖 = 𝑀))
11		csbeq1 3892	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑀 → ⦋𝑗 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
12	11	ineq2d 4208	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
13	12	eqeq1d 2729	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
14	10, 13	orbi12d 917	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
15	14	ralunsn 4890	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
16	15	ralbidv 3172	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
17		eqeq2 2739	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑀 = 𝑗 ↔ 𝑀 = 𝑀))
18	11	ineq2d 4208	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
19	18	eqeq1d 2729	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
20	17, 19	orbi12d 917	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
21	20	ralunsn 4890	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
22		eqid 2727	. . . . . . . . 9 ⊢ 𝑀 = 𝑀
23	22	orci 864	. . . . . . . 8 ⊢ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)
24	23	biantru 529	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
25	21, 24	bitr4di 289	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
26	16, 25	anbi12d 630	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ((∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
27	9, 26	bitrd 279	. . . 4 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
28		r19.26 3106	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
29		disjors 5123	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
30	29	anbi1i 623	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
31	28, 30	bitr4i 278	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
32	31	anbi1i 623	. . . 4 ⊢ ((∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
33	27, 32	bitrdi 287	. . 3 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
34	33	adantr 480	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
35		orcom 869	. . . . . . . . 9 ⊢ (((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
36	35	ralbii 3088	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
37		r19.30 3115	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
38		risset 3225	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)
39		biorf 935	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
40	38, 39	sylnbi 330	. . . . . . . . . . 11 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
41	40	adantl 481	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
42		orcom 869	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
43	41, 42	bitrdi 287	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)))
44	37, 43	imbitrrid 245	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
45	36, 44	biimtrrid 242	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
46		olc 867	. . . . . . . 8 ⊢ ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
47	46	ralimi 3078	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
48	45, 47	impbid1 224	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
49		nfv 1910	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝐵 ∩ 𝐶) = ∅
50		nfcsb1v 3914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
51		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
52	50, 51	nfin 4212	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶)
53	52	nfeq1 2913	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
54		csbeq1a 3903	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
55	54	ineq1d 4207	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝐵 ∩ 𝐶) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
56	55	eqeq1d 2729	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
57	49, 53, 56	cbvralw 3298	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
58	57	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
59		ss0b 4393	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
60		iunss 5042	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
61		iunin1 5069	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
62	61	eqeq1i 2732	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
63	59, 60, 62	3bitr3ri 302	. . . . . . . . . 10 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
64		ss0b 4393	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ 𝐶) ⊆ ∅ ↔ (𝐵 ∩ 𝐶) = ∅)
65	64	ralbii 3088	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
66	63, 65	bitri 275	. . . . . . . . 9 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
67	66	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅))
68		nfcvd 2899	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑥𝐶)
69		disjunsn.s	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)
70	68, 69	csbiegf 3923	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑥⦌𝐵 = 𝐶)
71	70	ineq2d 4208	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
72	71	eqeq1d 2729	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
73	72	ralbidv 3172	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
74	58, 67, 73	3bitr4d 311	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
75	74	adantr 480	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
76	48, 75	bitr4d 282	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
77	76	anbi2d 628	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
78		orcom 869	. . . . . . . 8 ⊢ (((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
79	78	ralbii 3088	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
80		r19.30 3115	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
81		clel5 3651	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)
82		biorf 935	. . . . . . . . . . 11 ⊢ (¬ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
83	81, 82	sylnbi 330	. . . . . . . . . 10 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
84	83	adantl 481	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
85		orcom 869	. . . . . . . . 9 ⊢ ((∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
86	84, 85	bitrdi 287	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)))
87	80, 86	imbitrrid 245	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
88	79, 87	biimtrrid 242	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
89		olc 867	. . . . . . 7 ⊢ ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
90	89	ralimi 3078	. . . . . 6 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
91	88, 90	impbid1 224	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
92		nfv 1910	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝐵 ∩ 𝐶) = ∅
93		nfcsb1v 3914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑗 / 𝑥⦌𝐵
94	93, 51	nfin 4212	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶)
95	94	nfeq1 2913	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
96		csbeq1a 3903	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑥⦌𝐵)
97	96	ineq1d 4207	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝐵 ∩ 𝐶) = (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶))
98	97	eqeq1d 2729	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
99	92, 95, 98	cbvralw 3298	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
100	99	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
101		incom 4197	. . . . . . . . . 10 ⊢ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵)
102	101	eqeq1i 2732	. . . . . . . . 9 ⊢ ((⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
103	102	ralbii 3088	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
104	100, 103	bitrdi 287	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
105	70	ineq1d 4207	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵))
106	105	eqeq1d 2729	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
107	106	ralbidv 3172	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
108	104, 67, 107	3bitr4d 311	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
109	108	adantr 480	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
110	91, 109	bitr4d 282	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
111	77, 110	anbi12d 630	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
112		anass 468	. . . 4 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
113		anidm 564	. . . . 5 ⊢ (((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
114	113	anbi2i 622	. . . 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 205 ∧ wa 395 ∨ wo 846 = wceq 1534 ∈ wcel 2099 ∀wral 3056 ∃wrex 3065 ⦋csb 3889 ∪ cun 3942 ∩ cin 3943 ⊆ wss 3944 ∅c0 4318 {csn 4624 ∪ ciun 4991 Disj wdisj 5107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ral 3057 df-rex 3066 df-rmo 3371 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-sn 4625 df-iun 4993 df-disj 5108

This theorem is referenced by: disjun0 32378 disjiunel 32379

W3C validator