Metamath Proof Explorer

Theorem xpdifcnvepel

Description: The set of couples in a Cartesian product, where the second is not an element of the first. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Assertion xpdifcnvepel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) = ( ( 𝐴 × 𝐵 ) ∖ ◡ E )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
2 1 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
3 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ∃ 𝑖 ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
4 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
5 4 exbii ⊢ ( ∃ 𝑖 ∃ 𝑥 ∈ 𝐴 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
6 2 3 5 3bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
7 eliun ⊢ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑝 ∈ ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) )
8 eldif ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ ◡ E ) )
9 opelxp ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) )
10 vex ⊢ 𝑖 ∈ V
11 vex ⊢ 𝑗 ∈ V
12 10 11 brcnv ⊢ ( 𝑖 ◡ E 𝑗 ↔ 𝑗 E 𝑖 )
13 df-br ⊢ ( 𝑖 ◡ E 𝑗 ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ◡ E )
14 epel ⊢ ( 𝑗 E 𝑖 ↔ 𝑗 ∈ 𝑖 )
15 12 13 14 3bitr3i ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ◡ E ↔ 𝑗 ∈ 𝑖 )
16 15 notbii ⊢ ( ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ ◡ E ↔ ¬ 𝑗 ∈ 𝑖 )
17 9 16 anbi12i ⊢ ( ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ¬ ⟨ 𝑖 , 𝑗 ⟩ ∈ ◡ E ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
18 8 17 bitri ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
19 18 anbi2i ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) ) )
20 19 2exbii ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) ) )
21 eldifi ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → 𝑝 ∈ ( 𝐴 × 𝐵 ) )
22 elxpi ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐵 ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) )
23 simpl ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
24 23 2eximi ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
25 21 22 24 3syl ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ )
26 25 ancli ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
27 19.42vv ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ ∃ 𝑖 ∃ 𝑗 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
28 26 27 sylibr ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) )
29 ancom ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) )
30 eleq1 ⊢ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) )
31 30 adantl ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) → ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) )
32 31 pm5.32da ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ) )
33 29 32 bitrid ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ) )
34 33 2exbidv ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ∧ 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) ) )
35 28 34 mpbid ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) → ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) )
36 30 biimpar ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) → 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) )
37 36 exlimivv ⊢ ( ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) → 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) )
38 35 37 impbii ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ) )
39 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
40 simprl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑖 ∈ { 𝑦 } )
41 40 elsnd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑖 = 𝑦 )
42 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑦 ∈ 𝐴 )
43 41 42 eqeltrd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑖 ∈ 𝐴 )
44 simprr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) )
45 44 eldifad ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → 𝑗 ∈ 𝐵 )
46 44 eldifbd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ¬ 𝑗 ∈ 𝑦 )
47 46 41 neleqtrrd ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ¬ 𝑗 ∈ 𝑖 )
48 43 45 47 jca31 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
49 48 adantll ⊢ ( ( ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
50 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
51 50 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑖 ∈ { 𝑥 } ↔ 𝑖 ∈ { 𝑦 } ) )
52 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∖ 𝑥 ) = ( 𝐵 ∖ 𝑦 ) )
53 52 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ↔ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) )
54 51 53 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ↔ ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) ) )
55 54 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) )
56 55 biimpi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐴 ( 𝑖 ∈ { 𝑦 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑦 ) ) )
57 49 56 r19.29a ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) → ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
58 simpll ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → 𝑖 ∈ 𝐴 )
59 vsnid ⊢ 𝑖 ∈ { 𝑖 }
60 59 a1i ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → 𝑖 ∈ { 𝑖 } )
61 simplr ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → 𝑗 ∈ 𝐵 )
62 simpr ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → ¬ 𝑗 ∈ 𝑖 )
63 61 62 eldifd ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → 𝑗 ∈ ( 𝐵 ∖ 𝑖 ) )
64 sneq ⊢ ( 𝑥 = 𝑖 → { 𝑥 } = { 𝑖 } )
65 64 eleq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑖 ∈ { 𝑥 } ↔ 𝑖 ∈ { 𝑖 } ) )
66 difeq2 ⊢ ( 𝑥 = 𝑖 → ( 𝐵 ∖ 𝑥 ) = ( 𝐵 ∖ 𝑖 ) )
67 66 eleq2d ⊢ ( 𝑥 = 𝑖 → ( 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ↔ 𝑗 ∈ ( 𝐵 ∖ 𝑖 ) ) )
68 65 67 anbi12d ⊢ ( 𝑥 = 𝑖 → ( ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ↔ ( 𝑖 ∈ { 𝑖 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑖 ) ) ) )
69 68 rspcev ⊢ ( ( 𝑖 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑖 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑖 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) )
70 58 60 63 69 syl12anc ⊢ ( ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) → ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) )
71 57 70 impbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ↔ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) )
72 71 anbi2i ⊢ ( ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ∃ 𝑥 ∈ 𝐴 ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) ) )
73 39 72 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) ) )
74 73 2exbii ⊢ ( ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ∧ ¬ 𝑗 ∈ 𝑖 ) ) )
75 20 38 74 3bitr4i ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) ↔ ∃ 𝑖 ∃ 𝑗 ∃ 𝑥 ∈ 𝐴 ( 𝑝 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ { 𝑥 } ∧ 𝑗 ∈ ( 𝐵 ∖ 𝑥 ) ) ) )
76 6 7 75 3bitr4i ⊢ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) ↔ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) ∖ ◡ E ) )
77 76 eqriv ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐵 ∖ 𝑥 ) ) = ( ( 𝐴 × 𝐵 ) ∖ ◡ E )