Theorem prnebg 4856

Description: A (proper) pair is not equal to another (maybe improper) pair if and only if an element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 16-Jan-2018.)

Assertion

Ref	Expression
prnebg	⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Proof of Theorem prnebg

Step	Hyp	Ref	Expression
1		prneimg 4855	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
2	1	3adant3 1132	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3		ioran 982	. . . . 5 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
4		ianor 980	. . . . . . 7 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷))
5		nne 2944	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶)
6		nne 2944	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷)
7	5, 6	orbi12i 913	. . . . . . 7 ⊢ ((¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
8	4, 7	bitri 274	. . . . . 6 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
9		ianor 980	. . . . . . 7 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷))
10		nne 2944	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶)
11		nne 2944	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷)
12	10, 11	orbi12i 913	. . . . . . 7 ⊢ ((¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
13	9, 12	bitri 274	. . . . . 6 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
14	8, 13	anbi12i 627	. . . . 5 ⊢ ((¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
15	3, 14	bitri 274	. . . 4 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
16		anddi 1009	. . . . 5 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))))
17		eqtr3 2758	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
18		eqneqall 2951	. . . . . . . . . 10 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
19	17, 18	syl 17	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20		preq12 4739	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
21	20	a1d 25	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
22	19, 21	jaoi 855	. . . . . . . 8 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23		preq12 4739	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24		prcom 4736	. . . . . . . . . . 11 ⊢ {𝐷, 𝐶} = {𝐶, 𝐷}
25	23, 24	eqtrdi 2788	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
26	25	a1d 25	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27		eqtr3 2758	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐵)
28	27, 18	syl 17	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
29	26, 28	jaoi 855	. . . . . . . 8 ⊢ (((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
30	22, 29	jaoi 855	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
31	30	com12 32	. . . . . 6 ⊢ (𝐴 ≠ 𝐵 → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32	31	3ad2ant3 1135	. . . . 5 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
33	16, 32	biimtrid 241	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
34	15, 33	biimtrid 241	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
35	34	necon1ad 2957	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
36	2, 35	impbid 211	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  {cpr 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  zlmodzxznm  47266