Theorem disjunsn 29407

Description: Append an element to a disjoint collection. Similar to ralunsn 4422, gsumunsn 18359, 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 4635	. . . . . 6 ⊢ (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
2		eqeq1 2626	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑀 = 𝑗))
3		csbeq1 3536	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑀 → ⦋𝑖 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
4	3	ineq1d 3813	. . . . . . . . . 10 ⊢ (𝑖 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵))
5	4	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑖 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
6	2, 5	orbi12d 746	. . . . . . . 8 ⊢ (𝑖 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
7	6	ralbidv 2986	. . . . . . 7 ⊢ (𝑖 = 𝑀 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
8	7	ralunsn 4422	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ (𝐴 ∪ {𝑀})∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
9	1, 8	syl5bb 272	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
10		eqeq2 2633	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑖 = 𝑗 ↔ 𝑖 = 𝑀))
11		csbeq1 3536	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑀 → ⦋𝑗 / 𝑥⦌𝐵 = ⦋𝑀 / 𝑥⦌𝐵)
12	11	ineq2d 3814	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
13	12	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
14	10, 13	orbi12d 746	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
15	14	ralunsn 4422	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
16	15	ralbidv 2986	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
17		eqeq2 2633	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → (𝑀 = 𝑗 ↔ 𝑀 = 𝑀))
18	11	ineq2d 3814	. . . . . . . . . 10 ⊢ (𝑗 = 𝑀 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵))
19	18	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑗 = 𝑀 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
20	17, 19	orbi12d 746	. . . . . . . 8 ⊢ (𝑗 = 𝑀 → ((𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
21	20	ralunsn 4422	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))))
22		eqid 2622	. . . . . . . . 9 ⊢ 𝑀 = 𝑀
23	22	orci 405	. . . . . . . 8 ⊢ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)
24	23	biantru 526	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑀 = 𝑀 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
25	21, 24	syl6bbr 278	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
26	16, 25	anbi12d 747	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ((∀𝑖 ∈ 𝐴 ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑗 ∈ (𝐴 ∪ {𝑀})(𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
27	9, 26	bitrd 268	. . . 4 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
28		r19.26 3064	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
29		disjors 4635	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
30	29	anbi1i 731	. . . . . 6 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
31	28, 30	bitr4i 267	. . . . 5 ⊢ (∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
32	31	anbi1i 731	. . . 4 ⊢ ((∀𝑖 ∈ 𝐴 (∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ∧ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
33	27, 32	syl6bb 276	. . 3 ⊢ (𝑀 ∈ 𝑉 → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
34	33	adantr 481	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))))
35		orcom 402	. . . . . . . . 9 ⊢ (((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
36	35	ralbii 2980	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) ↔ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
37		r19.30 3082	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
38		risset 3062	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)
39		biorf 420	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
40	38, 39	sylnbi 320	. . . . . . . . . . 11 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
41	40	adantl 482	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)))
42		orcom 402	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀))
43	41, 42	syl6bb 276	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑖 ∈ 𝐴 𝑖 = 𝑀)))
44	37, 43	syl5ibr 236	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ∨ 𝑖 = 𝑀) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
45	36, 44	syl5bir 233	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) → ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
46		olc 399	. . . . . . . 8 ⊢ ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
47	46	ralimi 2952	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ → ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
48	45, 47	impbid1 215	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
49		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝐵 ∩ 𝐶) = ∅
50		nfcsb1v 3549	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
51		nfcv 2764	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐶
52	50, 51	nfin 3820	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶)
53	52	nfeq1 2778	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
54		csbeq1a 3542	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
55	54	ineq1d 3813	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝐵 ∩ 𝐶) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
56	55	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
57	49, 53, 56	cbvral 3167	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
58	57	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
59		ss0b 3973	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
60		iunss 4561	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
61		iunin1 4585	. . . . . . . . . . . 12 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶)
62	61	eqeq1i 2627	. . . . . . . . . . 11 ⊢ (∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
63	59, 60, 62	3bitr3ri 291	. . . . . . . . . 10 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅)
64		ss0b 3973	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ 𝐶) ⊆ ∅ ↔ (𝐵 ∩ 𝐶) = ∅)
65	64	ralbii 2980	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) ⊆ ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
66	63, 65	bitri 264	. . . . . . . . 9 ⊢ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅)
67	66	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅))
68		nfcvd 2765	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → Ⅎ𝑥𝐶)
69		disjunsn.s	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑀 → 𝐵 = 𝐶)
70	68, 69	csbiegf 3557	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ⦋𝑀 / 𝑥⦌𝐵 = 𝐶)
71	70	ineq2d 3814	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶))
72	71	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
73	72	ralbidv 2986	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
74	58, 67, 73	3bitr4d 300	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
75	74	adantr 481	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑖 ∈ 𝐴 (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅))
76	48, 75	bitr4d 271	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
77	76	anbi2d 740	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
78		orcom 402	. . . . . . . 8 ⊢ (((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
79	78	ralbii 2980	. . . . . . 7 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) ↔ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
80		r19.30 3082	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
81		clel5 3343	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝐴 ↔ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)
82		biorf 420	. . . . . . . . . . 11 ⊢ (¬ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
83	81, 82	sylnbi 320	. . . . . . . . . 10 ⊢ (¬ 𝑀 ∈ 𝐴 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
84	83	adantl 482	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)))
85		orcom 402	. . . . . . . . 9 ⊢ ((∃𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗))
86	84, 85	syl6bb 276	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ ∃𝑗 ∈ 𝐴 𝑀 = 𝑗)))
87	80, 86	syl5ibr 236	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ∨ 𝑀 = 𝑗) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
88	79, 87	syl5bir 233	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) → ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
89		olc 399	. . . . . . 7 ⊢ ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
90	89	ralimi 2952	. . . . . 6 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ → ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
91	88, 90	impbid1 215	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
92		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝐵 ∩ 𝐶) = ∅
93		nfcsb1v 3549	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⦋𝑗 / 𝑥⦌𝐵
94	93, 51	nfin 3820	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶)
95	94	nfeq1 2778	. . . . . . . . . 10 ⊢ Ⅎ𝑥(⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅
96		csbeq1a 3542	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑥⦌𝐵)
97	96	ineq1d 3813	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (𝐵 ∩ 𝐶) = (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶))
98	97	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → ((𝐵 ∩ 𝐶) = ∅ ↔ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
99	92, 95, 98	cbvral 3167	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅)
100	99	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅))
101		incom 3805	. . . . . . . . . 10 ⊢ (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵)
102	101	eqeq1i 2627	. . . . . . . . 9 ⊢ ((⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
103	102	ralbii 2980	. . . . . . . 8 ⊢ (∀𝑗 ∈ 𝐴 (⦋𝑗 / 𝑥⦌𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)
104	100, 103	syl6bb 276	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
105	70	ineq1d 3813	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵))
106	105	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ((⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
107	106	ralbidv 2986	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → (∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅ ↔ ∀𝑗 ∈ 𝐴 (𝐶 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
108	104, 67, 107	3bitr4d 300	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
109	108	adantr 481	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ↔ ∀𝑗 ∈ 𝐴 (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅))
110	91, 109	bitr4d 271	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
111	77, 110	anbi12d 747	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
112		anass 681	. . . 4 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
113		anidm 676	. . . . 5 ⊢ (((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)
114	113	anbi2i 730	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ((∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅ ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
115	112, 114	bitri 264	. . 3 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅))
116	111, 115	syl6bb 276	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑖 ∈ 𝐴 (𝑖 = 𝑀 ∨ (⦋𝑖 / 𝑥⦌𝐵 ∩ ⦋𝑀 / 𝑥⦌𝐵) = ∅)) ∧ ∀𝑗 ∈ 𝐴 (𝑀 = 𝑗 ∨ (⦋𝑀 / 𝑥⦌𝐵 ∩ ⦋𝑗 / 𝑥⦌𝐵) = ∅)) ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))
117	34, 116	bitrd 268	1 ⊢ ((𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴) → (Disj 𝑥 ∈ (𝐴 ∪ {𝑀})𝐵 ↔ (Disj 𝑥 ∈ 𝐴 𝐵 ∧ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶) = ∅)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  ⦋csb 3533   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  {csn 4177  ∪ ciun 4520  Disj wdisj 4620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-iun 4522  df-disj 4621

This theorem is referenced by:  disjun0  29408  disjiunel  29409