Theorem prnebg 4815

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 4813	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
2	1	3adant3 1150	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷}))
3		ioran 999	. . . . 5 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))
4		ianor 997	. . . . . . 7 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷))
5		nne 2959	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶)
6		nne 2959	. . . . . . . 8 ⊢ (¬ 𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷)
7	5, 6	orbi12i 928	. . . . . . 7 ⊢ ((¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
8	4, 7	bitri 278	. . . . . 6 ⊢ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))
9		ianor 997	. . . . . . 7 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷))
10		nne 2959	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶)
11		nne 2959	. . . . . . . 8 ⊢ (¬ 𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷)
12	10, 11	orbi12i 928	. . . . . . 7 ⊢ ((¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
13	9, 12	bitri 278	. . . . . 6 ⊢ (¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))
14	8, 13	anbi12i 640	. . . . 5 ⊢ ((¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
15	3, 14	bitri 278	. . . 4 ⊢ (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))
16		anddi 1028	. . . . 5 ⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))))
17		eqtr3 2782	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
18		eqneqall 2966	. . . . . . . . . 10 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
19	17, 18	syl 18	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
20		preq12 4695	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
21	20	a1d 26	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
22	19, 21	jaoi 871	. . . . . . . 8 ⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
23		preq12 4695	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐷, 𝐶})
24		prcom 4692	. . . . . . . . . . 11 ⊢ {𝐷, 𝐶} = {𝐶, 𝐷}
25	23, 24	eqtrdi 2811	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → {𝐴, 𝐵} = {𝐶, 𝐷})
26	25	a1d 26	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
27		eqtr3 2782	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐵)
28	27, 18	syl 18	. . . . . . . . 9 ⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
29	26, 28	jaoi 871	. . . . . . . 8 ⊢ (((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
30	22, 29	jaoi 871	. . . . . . 7 ⊢ ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → (𝐴 ≠ 𝐵 → {𝐴, 𝐵} = {𝐶, 𝐷}))
31	30	com12 33	. . . . . 6 ⊢ (𝐴 ≠ 𝐵 → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
32	31	3ad2ant3 1153	. . . . 5 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) ∨ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐷))) → {𝐴, 𝐵} = {𝐶, 𝐷}))
33	16, 32	biimtrid 245	. . . 4 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
34	15, 33	biimtrid 245	. . 3 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} = {𝐶, 𝐷}))
35	34	necon1ad 2972	. 2 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} ≠ {𝐶, 𝐷} → ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))))
36	2, 35	impbid 215	1 ⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ {𝐴, 𝐵} ≠ {𝐶, 𝐷}))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  {cpr 4585

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-un 3903  df-sn 4584  df-pr 4586

This theorem is used by:  zlmodzxznm  49531