Theorem bnj1533 30922

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

Hypotheses

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

Assertion

Ref	Expression
bnj1533	|- ( th -> A. z e. B C = E )

Proof of Theorem bnj1533

Step	Hyp	Ref	Expression
1		bnj1533.1	. . . 4 |- ( th -> A. z e. B -. z e. D )
2	1	bnj1211 30868	. . 3 |- ( th -> A. z ( z e. B -> -. z e. D ) )
3		bnj1533.3	. . . . . . . 8 |- D = { z e. A | C =/= E }
4	3	rabeq2i 3197	. . . . . . 7 |- ( z e. D <-> ( z e. A /\ C =/= E ) )
5	4	notbii 310	. . . . . 6 |- ( -. z e. D <-> -. ( z e. A /\ C =/= E ) )
6		imnan 438	. . . . . 6 |- ( ( z e. A -> -. C =/= E ) <-> -. ( z e. A /\ C =/= E ) )
7		nne 2798	. . . . . . 7 |- ( -. C =/= E <-> C = E )
8	7	imbi2i 326	. . . . . 6 |- ( ( z e. A -> -. C =/= E ) <-> ( z e. A -> C = E ) )
9	5, 6, 8	3bitr2i 288	. . . . 5 |- ( -. z e. D <-> ( z e. A -> C = E ) )
10	9	imbi2i 326	. . . 4 |- ( ( z e. B -> -. z e. D ) <-> ( z e. B -> ( z e. A -> C = E ) ) )
11		bnj1533.2	. . . . . . 7 |- B C_ A
12	11	sseli 3599	. . . . . 6 |- ( z e. B -> z e. A )
13	12	imim1i 63	. . . . 5 |- ( ( z e. A -> C = E ) -> ( z e. B -> C = E ) )
14		ax-1 6	. . . . . . . . 9 |- ( ( z e. A -> C = E ) -> ( z e. B -> ( z e. A -> C = E ) ) )
15	14	anim1i 592	. . . . . . . 8 |- ( ( ( z e. A -> C = E ) /\ z e. B ) -> ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) )
16		simpr 477	. . . . . . . . . 10 |- ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> z e. B )
17		simpl 473	. . . . . . . . . 10 |- ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( z e. B -> ( z e. A -> C = E ) ) )
18	16, 17	mpd 15	. . . . . . . . 9 |- ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( z e. A -> C = E ) )
19	18, 16	jca 554	. . . . . . . 8 |- ( ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) -> ( ( z e. A -> C = E ) /\ z e. B ) )
20	15, 19	impbii 199	. . . . . . 7 |- ( ( ( z e. A -> C = E ) /\ z e. B ) <-> ( ( z e. B -> ( z e. A -> C = E ) ) /\ z e. B ) )
21	20	imbi1i 339	. . . . . 6 |- ( ( ( ( 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 462	. . . . . 6 |- ( ( ( ( z e. A -> C = E ) /\ z e. B ) -> C = E ) <-> ( ( z e. A -> C = E ) -> ( z e. B -> C = E ) ) )
23		impexp 462	. . . . . 6 |- ( ( ( ( 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 290	. . . . 5 |- ( ( ( 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 220	. . . 4 |- ( ( z e. B -> ( z e. A -> C = E ) ) -> ( z e. B -> C = E ) )
26	10, 25	sylbi 207	. . 3 |- ( ( z e. B -> -. z e. D ) -> ( z e. B -> C = E ) )
27	2, 26	sylg 1750	. 2 |- ( th -> A. z ( z e. B -> C = E ) )
28	27	bnj1142 30860	1 |- ( th -> A. z e. B C = E )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   {crab 2916   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-ral 2917  df-rab 2921  df-in 3581  df-ss 3588

This theorem is referenced by:  bnj1523  31139