Definition df-rex

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of TakeutiZaring p. 22.

Note: This notation is most often used to express that ph holds for at least one element of a given class A . For this reading F/_ x A is required, though, for example, asserted when x and A are disjoint.

Should instead A depend on x , you rather assert at least one x fulfilling ph happens to be contained in the corresponding A ( x ) . This interpretation is rarely needed (see also df-ral ). (Contributed by NM, 30-Aug-1993)

	Ref	Expression
Assertion	df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		wph	|- ph
3	2 0 1	wrex	|- E. x e. A ph
4	0	cv	|- x
5	4 1	wcel	|- x e. A
6	5 2	wa	|- ( x e. A /\ ph )
7	6 0	wex	|- E. x ( x e. A /\ ph )
8	3 7	wb	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )