ax4e - Higher-Order Logic Explorer

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

Theorem ax4e 158

Description: Existential introduction.

**Hypotheses**
Ref	Expression
ax4e.1
ax4e.2

**Assertion**
Ref	Expression
ax4e

Proof of Theorem ax4e Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wv 58	. . . . 5
2		ax4e.1	. . . . . . 7
3		ax4e.2	. . . . . . 7
4	2, 3	wc 45	. . . . . 6
5		wal 124	. . . . . . 7
6		wim 127	. . . . . . . . 9
7		wv 58	. . . . . . . . . 10
8	2, 7	wc 45	. . . . . . . . 9
9	6, 8, 1	wov 64	. . . . . . . 8
10	9	wl 59	. . . . . . 7
11	5, 10	wc 45	. . . . . 6
12	4, 11	simpl 22	. . . . 5
13	7, 3	weqi 68	. . . . . . . . . 10
14	13	id 25	. . . . . . . . 9
15	2, 7, 14	ceq2 80	. . . . . . . 8
16	6, 8, 1, 15	oveq1 89	. . . . . . 7
17	9, 3, 16	cla4v 142	. . . . . 6
18	17, 4	adantl 51	. . . . 5
19	1, 12, 18	mpd 146	. . . 4
20	19	ex 148	. . 3
21	20	alrimiv 141	. 2
22	2	exval 133	. . 3
23	4, 22	a1i 28	. 2
24	21, 23	mpbir 77	1