This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ichexmpl1

Description: Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023)

Ref Expression
Assertion ichexmpl1 
|- [ a <> b ] E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c )

Proof

Step Hyp Ref Expression
1 equequ1 
 |-  ( a = t -> ( a = b <-> t = b ) )
2 neeq1 
 |-  ( a = t -> ( a =/= c <-> t =/= c ) )
3 1 2 3anbi12d 
 |-  ( a = t -> ( ( a = b /\ a =/= c /\ b =/= c ) <-> ( t = b /\ t =/= c /\ b =/= c ) ) )
4 3 2exbidv 
 |-  ( a = t -> ( E. b E. c ( a = b /\ a =/= c /\ b =/= c ) <-> E. b E. c ( t = b /\ t =/= c /\ b =/= c ) ) )
5 4 cbvexvw 
 |-  ( E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) <-> E. t E. b E. c ( t = b /\ t =/= c /\ b =/= c ) )
6 5 a1i 
 |-  ( a = t -> ( E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) <-> E. t E. b E. c ( t = b /\ t =/= c /\ b =/= c ) ) )
7 equequ2 
 |-  ( b = a -> ( t = b <-> t = a ) )
8 neeq1 
 |-  ( b = a -> ( b =/= c <-> a =/= c ) )
9 7 8 3anbi13d 
 |-  ( b = a -> ( ( t = b /\ t =/= c /\ b =/= c ) <-> ( t = a /\ t =/= c /\ a =/= c ) ) )
10 9 exbidv 
 |-  ( b = a -> ( E. c ( t = b /\ t =/= c /\ b =/= c ) <-> E. c ( t = a /\ t =/= c /\ a =/= c ) ) )
11 10 cbvexvw 
 |-  ( E. b E. c ( t = b /\ t =/= c /\ b =/= c ) <-> E. a E. c ( t = a /\ t =/= c /\ a =/= c ) )
12 11 exbii 
 |-  ( E. t E. b E. c ( t = b /\ t =/= c /\ b =/= c ) <-> E. t E. a E. c ( t = a /\ t =/= c /\ a =/= c ) )
13 12 a1i 
 |-  ( b = a -> ( E. t E. b E. c ( t = b /\ t =/= c /\ b =/= c ) <-> E. t E. a E. c ( t = a /\ t =/= c /\ a =/= c ) ) )
14 equequ1 
 |-  ( t = b -> ( t = a <-> b = a ) )
15 neeq1 
 |-  ( t = b -> ( t =/= c <-> b =/= c ) )
16 14 15 3anbi12d 
 |-  ( t = b -> ( ( t = a /\ t =/= c /\ a =/= c ) <-> ( b = a /\ b =/= c /\ a =/= c ) ) )
17 16 2exbidv 
 |-  ( t = b -> ( E. a E. c ( t = a /\ t =/= c /\ a =/= c ) <-> E. a E. c ( b = a /\ b =/= c /\ a =/= c ) ) )
18 17 cbvexvw 
 |-  ( E. t E. a E. c ( t = a /\ t =/= c /\ a =/= c ) <-> E. b E. a E. c ( b = a /\ b =/= c /\ a =/= c ) )
19 excom 
 |-  ( E. b E. a E. c ( b = a /\ b =/= c /\ a =/= c ) <-> E. a E. b E. c ( b = a /\ b =/= c /\ a =/= c ) )
20 3ancomb 
 |-  ( ( b = a /\ b =/= c /\ a =/= c ) <-> ( b = a /\ a =/= c /\ b =/= c ) )
21 equcom 
 |-  ( b = a <-> a = b )
22 21 3anbi1i 
 |-  ( ( b = a /\ a =/= c /\ b =/= c ) <-> ( a = b /\ a =/= c /\ b =/= c ) )
23 20 22 bitri 
 |-  ( ( b = a /\ b =/= c /\ a =/= c ) <-> ( a = b /\ a =/= c /\ b =/= c ) )
24 23 3exbii 
 |-  ( E. a E. b E. c ( b = a /\ b =/= c /\ a =/= c ) <-> E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) )
25 19 24 bitri 
 |-  ( E. b E. a E. c ( b = a /\ b =/= c /\ a =/= c ) <-> E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) )
26 18 25 bitri 
 |-  ( E. t E. a E. c ( t = a /\ t =/= c /\ a =/= c ) <-> E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) )
27 26 a1i 
 |-  ( t = b -> ( E. t E. a E. c ( t = a /\ t =/= c /\ a =/= c ) <-> E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c ) ) )
28 6 13 27 ichcircshi 
 |-  [ a <> b ] E. a E. b E. c ( a = b /\ a =/= c /\ b =/= c )