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 32920

Description: Append an element to a disjoint collection. Similar to ralunsn 4860, gsumunsn 20031, 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 5093	. . . . . 6 ⊢ (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
2		eqeq1 2767	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑀 = 𝑗))
3		csbeq1 3857	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑀 → ⦋𝑖 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
4	3	ineq1d 4173	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵))
5	4	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
6	2, 5	orbi12d 931	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
7	6	ralbidv 3188	. . . . . . 7 ⊢ (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
8	7	ralunsn 4860	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
9	1, 8	bitrid 286	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
10		eqeq2 2775	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑖 = 𝑀))
11		csbeq1 3857	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑀 → ⦋𝑗 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
12	11	ineq2d 4174	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
13	12	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
14	10, 13	orbi12d 931	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
15	14	ralunsn 4860	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
16	15	ralbidv 3188	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
17		eqeq2 2775	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑀 = 𝑗 ↔ 𝑀 = 𝑀))
18	11	ineq2d 4174	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
19	18	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
20	17, 19	orbi12d 931	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
21	20	ralunsn 4860	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
22		eqid 2763	. . . . . . . . 9 ⊢ 𝑀 = 𝑀
23	22	orci 878	. . . . . . . 8 ⊢ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)
24	23	biantru 538	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
25	21, 24	bitr4di 292	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
26	16, 25	anbi12d 643	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ((∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
27	9, 26	bitrd 282	. . . 4 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
28		r19.26 3125	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
29		disjors 5093	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
30	29	anbi1i 635	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
31	28, 30	bitr4i 281	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
32	31	anbi1i 635	. . . 4 ⊢ ((∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
33	27, 32	bitrdi 290	. . 3 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
34	33	adantr 485	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
35		orcom 883	. . . . . . . . 9 ⊢ (((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
36	35	ralbii 3111	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
37		r19.30 3132	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
38		risset 3240	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)
39		biorf 949	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
40	38, 39	sylnbi 333	. . . . . . . . . . 11 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
41	40	adantl 486	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
42		orcom 883	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
43	41, 42	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)))
44	37, 43	imbitrrid 249	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
45	36, 44	biimtrrid 246	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
46		olc 881	. . . . . . . 8 ⊢ ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
47	46	ralimi 3102	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
48	45, 47	impbid1 228	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
49		nfv 1944	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝐵 ∩ 𝐶) = ∅
50		nfcsb1v 3878	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
51		nfcv 2925	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
52	50, 51	nfin 4178	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶)
53	52	nfeq1 2940	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
54		csbeq1a 3868	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
55	54	ineq1d 4173	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝐵 ∩ 𝐶) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
56	55	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
57	49, 53, 56	cbvralw 3307	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
58	57	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
59		ss0b 4359	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
60		iunss 5010	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
61		iunin1 5037	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
62	61	eqeq1i 2768	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
63	59, 60, 62	3bitr3ri 305	. . . . . . . . . 10 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
64		ss0b 4359	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ 𝐶) ⊆ ∅ ↔ (𝐵 ∩ 𝐶) = ∅)
65	64	ralbii 3111	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
66	63, 65	bitri 278	. . . . . . . . 9 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
67	66	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅))
68		nfcvd 2926	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑥𝐶)
69		disjunsn.s	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)
70	68, 69	csbiegf 3887	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑥⦌𝐵 = 𝐶)
71	70	ineq2d 4174	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
72	71	eqeq1d 2765	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
73	72	ralbidv 3188	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
74	58, 67, 73	3bitr4d 314	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
75	74	adantr 485	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
76	48, 75	bitr4d 285	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
77	76	anbi2d 641	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
78		orcom 883	. . . . . . . 8 ⊢ (((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
79	78	ralbii 3111	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
80		r19.30 3132	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
81		clel5 3625	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)
82		biorf 949	. . . . . . . . . . 11 ⊢ (¬ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
83	81, 82	sylnbi 333	. . . . . . . . . 10 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
84	83	adantl 486	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
85		orcom 883	. . . . . . . . 9 ⊢ ((∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
86	84, 85	bitrdi 290	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)))
87	80, 86	imbitrrid 249	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
88	79, 87	biimtrrid 246	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
89		olc 881	. . . . . . 7 ⊢ ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
90	89	ralimi 3102	. . . . . 6 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
91	88, 90	impbid1 228	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
92		nfv 1944	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝐵 ∩ 𝐶) = ∅
93		nfcsb1v 3878	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑗 / 𝑥⦌𝐵
94	93, 51	nfin 4178	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶)
95	94	nfeq1 2940	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
96		csbeq1a 3868	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑥⦌𝐵)
97	96	ineq1d 4173	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝐵 ∩ 𝐶) = (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶))
98	97	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
99	92, 95, 98	cbvralw 3307	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
100	99	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
101		incom 4163	. . . . . . . . . 10 ⊢ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵)
102	101	eqeq1i 2768	. . . . . . . . 9 ⊢ ((⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
103	102	ralbii 3111	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
104	100, 103	bitrdi 290	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
105	70	ineq1d 4173	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵))
106	105	eqeq1d 2765	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
107	106	ralbidv 3188	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
108	104, 67, 107	3bitr4d 314	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
109	108	adantr 485	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
110	91, 109	bitr4d 285	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
111	77, 110	anbi12d 643	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
112		anass 473	. . . 4 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
113		anidm 574	. . . . 5 ⊢ (((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
114	113	anbi2i 634	. . . 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 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 ∀wral 3079 ∃wrex 3089 ⦋csb 3854 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 {csn 4590 ∪ ciun 4957 Disj wdisj 5077

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ral 3080 df-rex 3090 df-rmo 3369 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-sn 4591 df-iun 4959 df-disj 5078

This theorem is referenced by: disjun0 32921 disjiunel 32922

W3C validator