Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  axpow		Unicode version

---

Theorem axpow 208

Description: Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory.

Hypothesis

Ref	Expression
axpow.1

Assertion

Ref	Expression
axpow

Distinct variable groups:   ,   ,   ,,

---

Proof of Theorem axpow Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wtru 40	. . . . 5
2		wal 124	. . . . . 6
3		wim 127	. . . . . . . 8
4		wv 58	. . . . . . . . 9
5		wv 58	. . . . . . . . 9
6	4, 5	wc 45	. . . . . . . 8
7		axpow.1	. . . . . . . . 9
8	7, 5	wc 45	. . . . . . . 8
9	3, 6, 8	wov 64	. . . . . . 7
10	9	wl 59	. . . . . 6
11	2, 10	wc 45	. . . . 5
12	1, 11	simpl 22	. . . 4
13	12	ex 148	. . 3
14	13	alrimiv 141	. 2
15		wal 124	. . . 4
16		wv 58	. . . . . . 7
17	16, 4	wc 45	. . . . . 6
18	3, 11, 17	wov 64	. . . . 5
19	18	wl 59	. . . 4
20	15, 19	wc 45	. . 3
21	1	wl 59	. . 3
22	16, 21	weqi 68	. . . . . . . . 9
23	22	id 25	. . . . . . . 8
24	16, 4, 23	ceq1 79	. . . . . . 7
25		wv 58	. . . . . . . . . . 11
26	25, 4	weqi 68	. . . . . . . . . 10
27	26, 1	eqid 73	. . . . . . . . 9
28	1, 4, 27	cl 106	. . . . . . . 8
29	22, 28	a1i 28	. . . . . . 7
30	17, 24, 29	eqtri 85	. . . . . 6
31	3, 11, 17, 30	oveq2 91	. . . . 5
32	18, 31	leq 81	. . . 4
33	15, 19, 32	ceq2 80	. . 3
34	20, 21, 33	cla4ev 159	. 2
35	14, 34	syl 16	1

Colors of variables: type var term

Syntax hints:  tv 1   ht 2  hb 3  kc 5  kl 6   ke 7  kt 8  kbr 9   wffMMJ2 11  wffMMJ2t 12   tim 111  tal 112  tex 113

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103

This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119  df-ex 121

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator