Theorem prproe 4434

Description: For an element of a proper unordered pair of elements of a class V, there is another (different) element of the class V which is an element of the proper pair. (Contributed by AV, 18-Dec-2021.)

Assertion

Ref	Expression
prproe	|- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )

Distinct variable groups:   v, A   v, B   v, C   v, V

Proof of Theorem prproe

Step	Hyp	Ref	Expression
1		elpri 4197	. . 3 |- ( C e. { A , B } -> ( C = A \/ C = B ) )
2		simprrr 805	. . . . . . 7 |- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. V )
3		necom 2847	. . . . . . . . . 10 |- ( A =/= B <-> B =/= A )
4		neeq2 2857	. . . . . . . . . . . 12 |- ( A = C -> ( B =/= A <-> B =/= C ) )
5	4	eqcoms 2630	. . . . . . . . . . 11 |- ( C = A -> ( B =/= A <-> B =/= C ) )
6	5	biimpcd 239	. . . . . . . . . 10 |- ( B =/= A -> ( C = A -> B =/= C ) )
7	3, 6	sylbi 207	. . . . . . . . 9 |- ( A =/= B -> ( C = A -> B =/= C ) )
8	7	adantr 481	. . . . . . . 8 |- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = A -> B =/= C ) )
9	8	impcom 446	. . . . . . 7 |- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B =/= C )
10		eldifsn 4317	. . . . . . 7 |- ( B e. ( V \ { C } ) <-> ( B e. V /\ B =/= C ) )
11	2, 9, 10	sylanbrc 698	. . . . . 6 |- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. ( V \ { C } ) )
12		eleq1 2689	. . . . . . 7 |- ( v = B -> ( v e. { A , B } <-> B e. { A , B } ) )
13	12	adantl 482	. . . . . 6 |- ( ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) /\ v = B ) -> ( v e. { A , B } <-> B e. { A , B } ) )
14		prid2g 4296	. . . . . . . . 9 |- ( B e. V -> B e. { A , B } )
15	14	adantl 482	. . . . . . . 8 |- ( ( A e. V /\ B e. V ) -> B e. { A , B } )
16	15	adantl 482	. . . . . . 7 |- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> B e. { A , B } )
17	16	adantl 482	. . . . . 6 |- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. { A , B } )
18	11, 13, 17	rspcedvd 3317	. . . . 5 |- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
19	18	ex 450	. . . 4 |- ( C = A -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
20		simprrl 804	. . . . . . 7 |- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. V )
21		neeq2 2857	. . . . . . . . . . 11 |- ( B = C -> ( A =/= B <-> A =/= C ) )
22	21	eqcoms 2630	. . . . . . . . . 10 |- ( C = B -> ( A =/= B <-> A =/= C ) )
23	22	biimpcd 239	. . . . . . . . 9 |- ( A =/= B -> ( C = B -> A =/= C ) )
24	23	adantr 481	. . . . . . . 8 |- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = B -> A =/= C ) )
25	24	impcom 446	. . . . . . 7 |- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A =/= C )
26		eldifsn 4317	. . . . . . 7 |- ( A e. ( V \ { C } ) <-> ( A e. V /\ A =/= C ) )
27	20, 25, 26	sylanbrc 698	. . . . . 6 |- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. ( V \ { C } ) )
28		eleq1 2689	. . . . . . 7 |- ( v = A -> ( v e. { A , B } <-> A e. { A , B } ) )
29	28	adantl 482	. . . . . 6 |- ( ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) /\ v = A ) -> ( v e. { A , B } <-> A e. { A , B } ) )
30		prid1g 4295	. . . . . . . . 9 |- ( A e. V -> A e. { A , B } )
31	30	adantr 481	. . . . . . . 8 |- ( ( A e. V /\ B e. V ) -> A e. { A , B } )
32	31	adantl 482	. . . . . . 7 |- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> A e. { A , B } )
33	32	adantl 482	. . . . . 6 |- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. { A , B } )
34	27, 29, 33	rspcedvd 3317	. . . . 5 |- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
35	34	ex 450	. . . 4 |- ( C = B -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
36	19, 35	jaoi 394	. . 3 |- ( ( C = A \/ C = B ) -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
37	1, 36	syl 17	. 2 |- ( C e. { A , B } -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
38	37	3impib 1262	1 |- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   \ cdif 3571   {csn 4177   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  edglnl  26038