Theorem axunnd 3742

Description: A version of the Axiom of Union with no distinct variable conditions.

Assertion

Ref	Expression
axunnd	|- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)

Proof of Theorem axunnd

Step	Hyp	Ref	Expression
1		axunndlem1 3741	. . . 4 |- E.wA.y(E.w(y e. w /\ w e. z) -> y e. w)
2		eq6 826	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
3		eq6 826	. . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
4	2, 3	hban 704	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
5		eq6 826	. . . . . . 7 |- (-. A.x x = y -> A.y -. A.x x = y)
6		eq6 826	. . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
7	5, 6	hban 704	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
8		ax-17 925	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
9		ddeel1 1003	. . . . . . . . . 10 |- (-. A.x x = y -> (y e. w -> A.x y e. w))
10	9	adantr 306	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (y e. w -> A.x y e. w))
11		ddeel2 1004	. . . . . . . . . 10 |- (-. A.x x = z -> (w e. z -> A.x w e. z))
12	11	adantl 305	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. z -> A.x w e. z))
13	10, 12	hband 788	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ((y e. w /\ w e. z) -> A.x(y e. w /\ w e. z)))
14	8, 13	hbexd 791	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(y e. w /\ w e. z) -> A.xE.w(y e. w /\ w e. z)))
15	4, 14, 10	hbimd 787	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> ((E.w(y e. w /\ w e. z) -> y e. w) -> A.x(E.w(y e. w /\ w e. z) -> y e. w)))
16	7, 15	hbald 790	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y(E.w(y e. w /\ w e. z) -> y e. w) -> A.xA.y(E.w(y e. w /\ w e. z) -> y e. w)))
17		nd5 3736	. . . . . . . . 9 |- (-. A.x x = y -> (w = x -> A.y w = x))
18	17	adantr 306	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
19	18	imdistani 340	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
20		hba1 698	. . . . . . . . 9 |- (A.y w = x -> A.yA.y w = x)
21	7, 20	hban 704	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> A.y((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
22		a14b 820	. . . . . . . . . . . . 13 |- (w = x -> (y e. w <-> y e. x))
23		a13b 819	. . . . . . . . . . . . 13 |- (w = x -> (w e. z <-> x e. z))
24	22, 23	anbi12d 476	. . . . . . . . . . . 12 |- (w = x -> ((y e. w /\ w e. z) <-> (y e. x /\ x e. z)))
25	24	a1i 7	. . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> ((y e. w /\ w e. z) <-> (y e. x /\ x e. z))))
26	4, 13, 25	cbvexd 978	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.w(y e. w /\ w e. z) <-> E.x(y e. x /\ x e. z)))
27	26	adantr 306	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (E.w(y e. w /\ w e. z) <-> E.x(y e. x /\ x e. z)))
28	22	a4s 682	. . . . . . . . . 10 |- (A.y w = x -> (y e. w <-> y e. x))
29	28	adantl 305	. . . . . . . . 9 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (y e. w <-> y e. x))
30	27, 29	imbi12d 474	. . . . . . . 8 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> ((E.w(y e. w /\ w e. z) -> y e. w) <-> (E.x(y e. x /\ x e. z) -> y e. x)))
31	21, 30	biald 782	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> (A.y(E.w(y e. w /\ w e. z) -> y e. w) <-> A.y(E.x(y e. x /\ x e. z) -> y e. x)))
32	19, 31	syl 12	. . . . . 6 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (A.y(E.w(y e. w /\ w e. z) -> y e. w) <-> A.y(E.x(y e. x /\ x e. z) -> y e. x)))
33	32	exp 291	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> (A.y(E.w(y e. w /\ w e. z) -> y e. w) <-> A.y(E.x(y e. x /\ x e. z) -> y e. x))))
34	4, 16, 33	cbvexd 978	. . . 4 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.wA.y(E.w(y e. w /\ w e. z) -> y e. w) <-> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)))
35	1, 34	mpbii 168	. . 3 |- ((-. A.x x = y /\ -. A.x x = z) -> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x))
36	35	exp 291	. 2 |- (-. A.x x = y -> (-. A.x x = z -> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)))
37		eq5 824	. . . 4 |- (A.x x = y -> A.yA.x x = y)
38		eq5 824	. . . . . 6 |- (A.x x = y -> A.xA.x x = y)
39		eirrv 3449	. . . . . . . 8 |- -. y e. y
40		a14b 820	. . . . . . . . 9 |- (x = y -> (y e. x <-> y e. y))
41		pm3.26 256	. . . . . . . . 9 |- ((y e. x /\ x e. z) -> y e. x)
42	40, 41	syl5bi 183	. . . . . . . 8 |- (x = y -> ((y e. x /\ x e. z) -> y e. y))
43	39, 42	mtoi 94	. . . . . . 7 |- (x = y -> -. (y e. x /\ x e. z))
44	43	a4s 682	. . . . . 6 |- (A.x x = y -> -. (y e. x /\ x e. z))
45	38, 44	nexd 780	. . . . 5 |- (A.x x = y -> -. E.x(y e. x /\ x e. z))
46	45	pm2.21d 74	. . . 4 |- (A.x x = y -> (E.x(y e. x /\ x e. z) -> y e. x))
47	37, 46	19.21ai 740	. . 3 |- (A.x x = y -> A.y(E.x(y e. x /\ x e. z) -> y e. x))
48		19.8a 712	. . 3 |- (A.y(E.x(y e. x /\ x e. z) -> y e. x) -> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x))
49	47, 48	syl 12	. 2 |- (A.x x = y -> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x))
50		eq5 824	. . . 4 |- (A.x x = z -> A.yA.x x = z)
51		eq5 824	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
52		eirrv 3449	. . . . . . . 8 |- -. z e. z
53		a13b 819	. . . . . . . . 9 |- (x = z -> (x e. z <-> z e. z))
54		pm3.27 260	. . . . . . . . 9 |- ((y e. x /\ x e. z) -> x e. z)
55	53, 54	syl5bi 183	. . . . . . . 8 |- (x = z -> ((y e. x /\ x e. z) -> z e. z))
56	52, 55	mtoi 94	. . . . . . 7 |- (x = z -> -. (y e. x /\ x e. z))
57	56	a4s 682	. . . . . 6 |- (A.x x = z -> -. (y e. x /\ x e. z))
58	51, 57	nexd 780	. . . . 5 |- (A.x x = z -> -. E.x(y e. x /\ x e. z))
59	58	pm2.21d 74	. . . 4 |- (A.x x = z -> (E.x(y e. x /\ x e. z) -> y e. x))
60	50, 59	19.21ai 740	. . 3 |- (A.x x = z -> A.y(E.x(y e. x /\ x e. z) -> y e. x))
61	60, 48	syl 12	. 2 |- (A.x x = z -> E.xA.y(E.x(y e. x /\ x e. z) -> y e. x))
62	36, 49, 61	pm2.61ii 113	1 |- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678   = weq 797   e. wel 803

This theorem is referenced by:  zfcndun 3761

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-eprel 2122  df-fr 2169

metamath.org