Metamath Proof Explorer

Theorem disjsuc2

Description: Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023)

Ref Expression
Assertion disjsuc2 ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅

Proof

Step Hyp Ref Expression
1 disjressuc2 ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u R ⋉ E -1 ∩ A R ⋉ E -1 = ∅
2 disjecxrncnvep ⊢ u ∈ V ∧ A ∈ V → u R ⋉ E -1 ∩ A R ⋉ E -1 = ∅ ↔ u ∩ A = ∅ ∨ u R ∩ A R = ∅
3 2 el2v1 ⊢ A ∈ V → u R ⋉ E -1 ∩ A R ⋉ E -1 = ∅ ↔ u ∩ A = ∅ ∨ u R ∩ A R = ∅
4 3 ralbidv ⊢ A ∈ V → ∀ u ∈ A u R ⋉ E -1 ∩ A R ⋉ E -1 = ∅ ↔ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅
5 4 anbi2d ⊢ A ∈ V → ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u R ⋉ E -1 ∩ A R ⋉ E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅
6 1 5 bitrd ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅