Metamath Proof Explorer


Theorem brprcneu

Description: If A is a proper class and F is any class, then there is no unique set which is related to A through the binary relation F . (Contributed by Scott Fenton, 7-Oct-2017)

Ref Expression
Assertion brprcneu ¬ A V ¬ ∃! x A F x

Proof

Step Hyp Ref Expression
1 dtru ¬ y y = x
2 exnal y ¬ x = y ¬ y x = y
3 equcom x = y y = x
4 3 albii y x = y y y = x
5 2 4 xchbinx y ¬ x = y ¬ y y = x
6 1 5 mpbir y ¬ x = y
7 6 jctr F F y ¬ x = y
8 19.42v y F ¬ x = y F y ¬ x = y
9 7 8 sylibr F y F ¬ x = y
10 opprc1 ¬ A V A x =
11 10 eleq1d ¬ A V A x F F
12 opprc1 ¬ A V A y =
13 12 eleq1d ¬ A V A y F F
14 11 13 anbi12d ¬ A V A x F A y F F F
15 anidm F F F
16 14 15 bitrdi ¬ A V A x F A y F F
17 16 anbi1d ¬ A V A x F A y F ¬ x = y F ¬ x = y
18 17 exbidv ¬ A V y A x F A y F ¬ x = y y F ¬ x = y
19 11 18 imbi12d ¬ A V A x F y A x F A y F ¬ x = y F y F ¬ x = y
20 9 19 mpbiri ¬ A V A x F y A x F A y F ¬ x = y
21 df-br A F x A x F
22 df-br A F y A y F
23 21 22 anbi12i A F x A F y A x F A y F
24 23 anbi1i A F x A F y ¬ x = y A x F A y F ¬ x = y
25 24 exbii y A F x A F y ¬ x = y y A x F A y F ¬ x = y
26 20 21 25 3imtr4g ¬ A V A F x y A F x A F y ¬ x = y
27 26 eximdv ¬ A V x A F x x y A F x A F y ¬ x = y
28 exnal x ¬ y A F x A F y x = y ¬ x y A F x A F y x = y
29 exanali y A F x A F y ¬ x = y ¬ y A F x A F y x = y
30 29 exbii x y A F x A F y ¬ x = y x ¬ y A F x A F y x = y
31 breq2 x = y A F x A F y
32 31 mo4 * x A F x x y A F x A F y x = y
33 32 notbii ¬ * x A F x ¬ x y A F x A F y x = y
34 28 30 33 3bitr4ri ¬ * x A F x x y A F x A F y ¬ x = y
35 27 34 syl6ibr ¬ A V x A F x ¬ * x A F x
36 df-eu ∃! x A F x x A F x * x A F x
37 36 notbii ¬ ∃! x A F x ¬ x A F x * x A F x
38 imnan x A F x ¬ * x A F x ¬ x A F x * x A F x
39 37 38 bitr4i ¬ ∃! x A F x x A F x ¬ * x A F x
40 35 39 sylibr ¬ A V ¬ ∃! x A F x