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 rabeq2i
 |-  ( 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 )