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

Metamath Proof Explorer

Theorem bnj1533

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1533.1 
|- ( th -> A. z e. B -. z e. D )
bnj1533.2 
|- B C_ A
bnj1533.3 
|- D = { z e. A | C =/= E }
Assertion bnj1533 
|- ( th -> A. z e. B C = E )

Proof

Step Hyp Ref Expression
1 bnj1533.1 
 |-  ( th -> A. z e. B -. z e. D )
2 bnj1533.2 
 |-  B C_ A
3 bnj1533.3 
 |-  D = { z e. A | C =/= E }
4 1 bnj1211 
 |-  ( th -> A. z ( z e. B -> -. z e. D ) )
5 3 reqabi 
 |-  ( z e. D <-> ( z e. A /\ C =/= E ) )
6 5 notbii 
 |-  ( -. z e. D <-> -. ( z e. A /\ C =/= E ) )
7 imnan 
 |-  ( ( z e. A -> -. C =/= E ) <-> -. ( z e. A /\ C =/= E ) )
8 nne 
 |-  ( -. C =/= E <-> C = E )
9 8 imbi2i 
 |-  ( ( z e. A -> -. C =/= E ) <-> ( z e. A -> C = E ) )
10 6 7 9 3bitr2i 
 |-  ( -. z e. D <-> ( z e. A -> C = E ) )
11 10 imbi2i 
 |-  ( ( z e. B -> -. z e. D ) <-> ( z e. B -> ( z e. A -> C = E ) ) )
12 2 sseli 
 |-  ( z e. B -> z e. A )
13 12 imim1i 
 |-  ( ( z e. A -> C = E ) -> ( z e. B -> C = E ) )
14 ax-1 
 |-  ( ( z e. A -> C = E ) -> ( z e. B -> ( z e. A -> C = E ) ) )
15 14 anim1i 
 |-  ( ( ( z e. A -> C = E ) /\ z e. B ) -> ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) )
16 simpr 
 |-  ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> z e. B )
17 simpl 
 |-  ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( z e. B -> ( z e. A -> C = E ) ) )
18 16 17 mpd 
 |-  ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( z e. A -> C = E ) )
19 18 16 jca 
 |-  ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( ( z e. A -> C = E ) /\ z e. B ) )
20 15 19 impbii 
 |-  ( ( ( z e. A -> C = E ) /\ z e. B ) <-> ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) )
21 20 imbi1i 
 |-  ( ( ( ( z e. A -> C = E ) /\ z e. B ) -> C = E ) <-> ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> C = E ) )
22 impexp 
 |-  ( ( ( ( z e. A -> C = E ) /\ z e. B ) -> C = E ) <-> ( ( z e. A -> C = E ) -> ( z e. B -> C = E ) ) )
23 impexp 
 |-  ( ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> C = E ) <-> ( ( z e. B -> ( z e. A -> C = E ) ) -> ( z e. B -> C = E ) ) )
24 21 22 23 3bitr3i 
 |-  ( ( ( z e. A -> C = E ) -> ( z e. B -> C = E ) ) <-> ( ( z e. B -> ( z e. A -> C = E ) ) -> ( z e. B -> C = E ) ) )
25 13 24 mpbi 
 |-  ( ( z e. B -> ( z e. A -> C = E ) ) -> ( z e. B -> C = E ) )
26 11 25 sylbi 
 |-  ( ( z e. B -> -. z e. D ) -> ( z e. B -> C = E ) )
27 4 26 sylg 
 |-  ( th -> A. z ( z e. B -> C = E ) )
28 27 bnj1142 
 |-  ( th -> A. z e. B C = E )