Theorem prnebg 4212

Description: A (proper) pair is not equal to another (maybe inproper) 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 4211	. . 3
2	1	3adant3 1016	. 2
3		ioran 490	. . . . 5
4		ianor 488	. . . . . . 7
5		nne 2658	. . . . . . . 8
6		nne 2658	. . . . . . . 8
7	5, 6	orbi12i 521	. . . . . . 7
8	4, 7	bitri 249	. . . . . 6
9		ianor 488	. . . . . . 7
10		nne 2658	. . . . . . . 8
11		nne 2658	. . . . . . . 8
12	10, 11	orbi12i 521	. . . . . . 7
13	9, 12	bitri 249	. . . . . 6
14	8, 13	anbi12i 697	. . . . 5
15	3, 14	bitri 249	. . . 4
16		anddi 870	. . . . 5
17		eqtr3 2485	. . . . . . . . . 10
18		eqneqall 2664	. . . . . . . . . 10
19	17, 18	syl 16	. . . . . . . . 9
20		preq12 4111	. . . . . . . . . 10
21	20	a1d 25	. . . . . . . . 9
22	19, 21	jaoi 379	. . . . . . . 8
23		preq12 4111	. . . . . . . . . . 11
24		prcom 4108	. . . . . . . . . . 11
25	23, 24	syl6eq 2514	. . . . . . . . . 10
26	25	a1d 25	. . . . . . . . 9
27		eqtr3 2485	. . . . . . . . . 10
28	27, 18	syl 16	. . . . . . . . 9
29	26, 28	jaoi 379	. . . . . . . 8
30	22, 29	jaoi 379	. . . . . . 7
31	30	com12 31	. . . . . 6
32	31	3ad2ant3 1019	. . . . 5
33	16, 32	syl5bi 217	. . . 4
34	15, 33	syl5bi 217	. . 3
35	34	necon1ad 2673	. 2
36	2, 35	impbid 191	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  {cpr 4031

This theorem is referenced by:  zlmodzxznm  33098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032