Theorem brprcneu 5114

Description: If A is a proper class, then there is no unique binary relationship with A as the first element. (Contributed by Scott Fenton, 7-Oct-2017.)

Assertion

Ref	Expression
brprcneu	|- (-. A e. _V -> -. E!x A Fx)

Distinct variable groups:   x,A   x, F

Proof of Theorem brprcneu

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dtruex 4237	. . . . . . . . 9 |- E.y -. y = x
2		equcom 1590	. . . . . . . . . . 11 |- (x = y <-> y = x)
3	2	notbii 593	. . . . . . . . . 10 |- (-. x = y <-> -. y = x)
4	3	exbii 1493	. . . . . . . . 9 |- (E.y -. x = y <-> E.y -. y = x)
5	1, 4	mpbir 134	. . . . . . . 8 |- E.y -. x = y
6	5	jctr 298	. . . . . . 7 |- ( (/) e. F -> ( (/) e. F /\ E.y -. x = y))
7		19.42v 1783	. . . . . . 7 |- (E.y( (/) e. F /\ -. x = y) <-> ( (/) e. F /\ E.y -. x = y))
8	6, 7	sylibr 137	. . . . . 6 |- ( (/) e. F -> E.y( (/) e. F /\ -. x = y))
9		opprc1 3562	. . . . . . . 8 |- (-. A e. _V -> <.A , x >. = (/))
10	9	eleq1d 2103	. . . . . . 7 |- (-. A e. _V -> ( <.A , x >. e. F <-> (/) e. F))
11		opprc1 3562	. . . . . . . . . . . 12 |- (-. A e. _V -> <.A , y >. = (/))
12	11	eleq1d 2103	. . . . . . . . . . 11 |- (-. A e. _V -> ( <.A , y >. e. F <-> (/) e. F))
13	10, 12	anbi12d 442	. . . . . . . . . 10 |- (-. A e. _V -> (( <.A , x >. e. F /\ <.A , y >. e. F) <-> ( (/) e. F /\ (/) e. F)))
14		anidm 376	. . . . . . . . . 10 |- (( (/) e. F /\ (/) e. F) <-> (/) e. F)
15	13, 14	syl6bb 185	. . . . . . . . 9 |- (-. A e. _V -> (( <.A , x >. e. F /\ <.A , y >. e. F) <-> (/) e. F))
16	15	anbi1d 438	. . . . . . . 8 |- (-. A e. _V -> ((( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y) <-> ( (/) e. F /\ -. x = y)))
17	16	exbidv 1703	. . . . . . 7 |- (-. A e. _V -> (E.y(( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y) <-> E.y( (/) e. F /\ -. x = y)))
18	10, 17	imbi12d 223	. . . . . 6 |- (-. A e. _V -> (( <.A , x >. e. F -> E.y(( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y)) <-> ( (/) e. F -> E.y( (/) e. F /\ -. x = y))))
19	8, 18	mpbiri 157	. . . . 5 |- (-. A e. _V -> ( <.A , x >. e. F -> E.y(( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y)))
20		df-br 3756	. . . . 5 |- (A Fx <-> <.A , x >. e. F)
21		df-br 3756	. . . . . . . 8 |- (A Fy <-> <.A , y >. e. F)
22	20, 21	anbi12i 433	. . . . . . 7 |- ((A Fx /\ A Fy) <-> ( <.A , x >. e. F /\ <.A , y >. e. F))
23	22	anbi1i 431	. . . . . 6 |- (((A Fx /\ A Fy) /\ -. x = y) <-> (( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y))
24	23	exbii 1493	. . . . 5 |- (E.y((A Fx /\ A Fy) /\ -. x = y) <-> E.y(( <.A , x >. e. F /\ <.A , y >. e. F) /\ -. x = y))
25	19, 20, 24	3imtr4g 194	. . . 4 |- (-. A e. _V -> (A Fx -> E.y((A Fx /\ A Fy) /\ -. x = y)))
26	25	eximdv 1757	. . 3 |- (-. A e. _V -> (E.x A Fx -> E.xE.y((A Fx /\ A Fy) /\ -. x = y)))
27		exanaliim 1535	. . . . . 6 |- (E.y((A Fx /\ A Fy) /\ -. x = y) -> -. A.y((A Fx /\ A Fy) -> x = y))
28	27	eximi 1488	. . . . 5 |- (E.xE.y((A Fx /\ A Fy) /\ -. x = y) -> E.x -. A.y((A Fx /\ A Fy) -> x = y))
29		exnalim 1534	. . . . 5 |- (E.x -. A.y((A Fx /\ A Fy) -> x = y) -> -. A.xA.y((A Fx /\ A Fy) -> x = y))
30	28, 29	syl 14	. . . 4 |- (E.xE.y((A Fx /\ A Fy) /\ -. x = y) -> -. A.xA.y((A Fx /\ A Fy) -> x = y))
31		breq2 3759	. . . . . 6 |- (x = y -> (A Fx <-> A Fy))
32	31	mo4 1958	. . . . 5 |- (E*x A Fx <-> A.xA.y((A Fx /\ A Fy) -> x = y))
33	32	notbii 593	. . . 4 |- (-. E*x A Fx <-> -. A.xA.y((A Fx /\ A Fy) -> x = y))
34	30, 33	sylibr 137	. . 3 |- (E.xE.y((A Fx /\ A Fy) /\ -. x = y) -> -. E*x A Fx)
35	26, 34	syl6 29	. 2 |- (-. A e. _V -> (E.x A Fx -> -. E*x A Fx))
36		eu5 1944	. . . 4 |- (E!x A Fx <-> (E.x A Fx /\ E*x A Fx))
37	36	notbii 593	. . 3 |- (-. E!x A Fx <-> -. (E.x A Fx /\ E*x A Fx))
38		imnan 623	. . 3 |- ((E.x A Fx -> -. E*x A Fx) <-> -. (E.x A Fx /\ E*x A Fx))
39	37, 38	bitr4i 176	. 2 |- (-. E!x A Fx <-> (E.x A Fx -> -. E*x A Fx))
40	35, 39	sylibr 137	1 |- (-. A e. _V -> -. E!x A Fx)

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97  A.wal 1240  E.wex 1378   e. wcel 1390  E!weu 1897  E*wmo 1898   _Vcvv 2551   (/)c0 3218   <.cop 3370   class class class wbr 3755

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756

This theorem is referenced by:  fvprc  5115