Metamath Proof Explorer

Theorem 2nreu

Description: If there are two different sets fulfilling a wff (by implicit substitution), then there is no unique set fulfilling the wff. (Contributed by AV, 20-Jun-2023)

Ref Expression
Hypotheses 2nreu.a 
|- ( x = A -> ( ph <-> ps ) )
2nreu.b 
|- ( x = B -> ( ph <-> ch ) )
Assertion 2nreu 
|- ( ( A e. X /\ B e. X /\ A =/= B ) -> ( ( ps /\ ch ) -> -. E! x e. X ph ) )

Proof

Step Hyp Ref Expression
1 2nreu.a 
 |-  ( x = A -> ( ph <-> ps ) )
2 2nreu.b 
 |-  ( x = B -> ( ph <-> ch ) )
3 simpl1 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> A e. X )
4 simpl2 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> B e. X )
5 simprl 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> ps )
6 2 sbcieg 
 |-  ( B e. X -> ( [. B / x ]. ph <-> ch ) )
7 6 3ad2ant2 
 |-  ( ( A e. X /\ B e. X /\ A =/= B ) -> ( [. B / x ]. ph <-> ch ) )
8 7 biimprd 
 |-  ( ( A e. X /\ B e. X /\ A =/= B ) -> ( ch -> [. B / x ]. ph ) )
9 8 adantld 
 |-  ( ( A e. X /\ B e. X /\ A =/= B ) -> ( ( ps /\ ch ) -> [. B / x ]. ph ) )
10 9 imp 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> [. B / x ]. ph )
11 5 10 jca 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> ( ps /\ [. B / x ]. ph ) )
12 simpl3 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> A =/= B )
13 simp1 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> A e. X )
14 simp2 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> B e. X )
15 simp3 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) )
16 sbcan 
 |-  ( [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> ( [. A / x ]. ( ph /\ [ y / x ] ph ) /\ [. A / x ]. x =/= y ) )
17 sbcan 
 |-  ( [. A / x ]. ( ph /\ [ y / x ] ph ) <-> ( [. A / x ]. ph /\ [. A / x ]. [ y / x ] ph ) )
18 1 sbcieg 
 |-  ( A e. X -> ( [. A / x ]. ph <-> ps ) )
19 nfs1v 
 |-  F/ x [ y / x ] ph
20 19 sbcgf 
 |-  ( A e. X -> ( [. A / x ]. [ y / x ] ph <-> [ y / x ] ph ) )
21 18 20 anbi12d 
 |-  ( A e. X -> ( ( [. A / x ]. ph /\ [. A / x ]. [ y / x ] ph ) <-> ( ps /\ [ y / x ] ph ) ) )
22 17 21 bitrid 
 |-  ( A e. X -> ( [. A / x ]. ( ph /\ [ y / x ] ph ) <-> ( ps /\ [ y / x ] ph ) ) )
23 sbcne12 
 |-  ( [. A / x ]. x =/= y <-> [_ A / x ]_ x =/= [_ A / x ]_ y )
24 csbvarg 
 |-  ( A e. X -> [_ A / x ]_ x = A )
25 csbconstg 
 |-  ( A e. X -> [_ A / x ]_ y = y )
26 24 25 neeq12d 
 |-  ( A e. X -> ( [_ A / x ]_ x =/= [_ A / x ]_ y <-> A =/= y ) )
27 23 26 bitrid 
 |-  ( A e. X -> ( [. A / x ]. x =/= y <-> A =/= y ) )
28 22 27 anbi12d 
 |-  ( A e. X -> ( ( [. A / x ]. ( ph /\ [ y / x ] ph ) /\ [. A / x ]. x =/= y ) <-> ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) ) )
29 16 28 bitrid 
 |-  ( A e. X -> ( [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) ) )
30 29 3ad2ant1 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) ) )
31 30 sbcbidv 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. B / y ]. [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> [. B / y ]. ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) ) )
32 sbcan 
 |-  ( [. B / y ]. ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) <-> ( [. B / y ]. ( ps /\ [ y / x ] ph ) /\ [. B / y ]. A =/= y ) )
33 sbcan 
 |-  ( [. B / y ]. ( ps /\ [ y / x ] ph ) <-> ( [. B / y ]. ps /\ [. B / y ]. [ y / x ] ph ) )
34 sbcg 
 |-  ( B e. X -> ( [. B / y ]. ps <-> ps ) )
35 sbsbc 
 |-  ( [ y / x ] ph <-> [. y / x ]. ph )
36 35 sbcbii 
 |-  ( [. B / y ]. [ y / x ] ph <-> [. B / y ]. [. y / x ]. ph )
37 sbccow 
 |-  ( [. B / y ]. [. y / x ]. ph <-> [. B / x ]. ph )
38 37 a1i 
 |-  ( B e. X -> ( [. B / y ]. [. y / x ]. ph <-> [. B / x ]. ph ) )
39 36 38 bitrid 
 |-  ( B e. X -> ( [. B / y ]. [ y / x ] ph <-> [. B / x ]. ph ) )
40 34 39 anbi12d 
 |-  ( B e. X -> ( ( [. B / y ]. ps /\ [. B / y ]. [ y / x ] ph ) <-> ( ps /\ [. B / x ]. ph ) ) )
41 40 3ad2ant2 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( ( [. B / y ]. ps /\ [. B / y ]. [ y / x ] ph ) <-> ( ps /\ [. B / x ]. ph ) ) )
42 33 41 bitrid 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. B / y ]. ( ps /\ [ y / x ] ph ) <-> ( ps /\ [. B / x ]. ph ) ) )
43 sbcne12 
 |-  ( [. B / y ]. A =/= y <-> [_ B / y ]_ A =/= [_ B / y ]_ y )
44 csbconstg 
 |-  ( B e. X -> [_ B / y ]_ A = A )
45 csbvarg 
 |-  ( B e. X -> [_ B / y ]_ y = B )
46 44 45 neeq12d 
 |-  ( B e. X -> ( [_ B / y ]_ A =/= [_ B / y ]_ y <-> A =/= B ) )
47 46 3ad2ant2 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [_ B / y ]_ A =/= [_ B / y ]_ y <-> A =/= B ) )
48 43 47 bitrid 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. B / y ]. A =/= y <-> A =/= B ) )
49 42 48 anbi12d 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( ( [. B / y ]. ( ps /\ [ y / x ] ph ) /\ [. B / y ]. A =/= y ) <-> ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) )
50 32 49 bitrid 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. B / y ]. ( ( ps /\ [ y / x ] ph ) /\ A =/= y ) <-> ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) )
51 31 50 bitrd 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> ( [. B / y ]. [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) )
52 15 51 mpbird 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> [. B / y ]. [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
53 rspesbca 
 |-  ( ( B e. X /\ [. B / y ]. [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) ) -> E. y e. X [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
54 14 52 53 syl2anc 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> E. y e. X [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
55 sbcrex 
 |-  ( [. A / x ]. E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) <-> E. y e. X [. A / x ]. ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
56 54 55 sylibr 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> [. A / x ]. E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
57 rspesbca 
 |-  ( ( A e. X /\ [. A / x ]. E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) ) -> E. x e. X E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
58 13 56 57 syl2anc 
 |-  ( ( A e. X /\ B e. X /\ ( ( ps /\ [. B / x ]. ph ) /\ A =/= B ) ) -> E. x e. X E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
59 3 4 11 12 58 syl112anc 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> E. x e. X E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
60 pm4.61 
 |-  ( -. ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ [ y / x ] ph ) /\ -. x = y ) )
61 df-ne 
 |-  ( x =/= y <-> -. x = y )
62 61 bicomi 
 |-  ( -. x = y <-> x =/= y )
63 62 anbi2i 
 |-  ( ( ( ph /\ [ y / x ] ph ) /\ -. x = y ) <-> ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
64 60 63 bitri 
 |-  ( -. ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
65 64 2rexbii 
 |-  ( E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> E. x e. X E. y e. X ( ( ph /\ [ y / x ] ph ) /\ x =/= y ) )
66 59 65 sylibr 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) )
67 66 olcd 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> ( -. E. x e. X ph \/ E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
68 ianor 
 |-  ( -. ( E. x e. X ph /\ A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( -. E. x e. X ph \/ -. A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
69 rexnal2 
 |-  ( E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> -. A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) )
70 69 bicomi 
 |-  ( -. A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) )
71 70 orbi2i 
 |-  ( ( -. E. x e. X ph \/ -. A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( -. E. x e. X ph \/ E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
72 68 71 bitri 
 |-  ( -. ( E. x e. X ph /\ A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( -. E. x e. X ph \/ E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
73 reu2 
 |-  ( E! x e. X ph <-> ( E. x e. X ph /\ A. x e. X A. y e. X ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
74 72 73 xchnxbir 
 |-  ( -. E! x e. X ph <-> ( -. E. x e. X ph \/ E. x e. X E. y e. X -. ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
75 67 74 sylibr 
 |-  ( ( ( A e. X /\ B e. X /\ A =/= B ) /\ ( ps /\ ch ) ) -> -. E! x e. X ph )
76 75 ex 
 |-  ( ( A e. X /\ B e. X /\ A =/= B ) -> ( ( ps /\ ch ) -> -. E! x e. X ph ) )