Theorem dfralseu2 17176

Description: The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17142. (Contributed by David A. Wheeler, 22-Jul-2026.)

Assertion

Ref	Expression
dfralseu2	|- ( A.E! x e. A ( ph -> ps ) <-> A.E! x ( ( x e. A /\ ph ) -> ps ) )

Proof of Theorem dfralseu2

Step	Hyp	Ref	Expression
1		df-ral 2533	. . . 4 |- ( A. x e. A ( ph -> ps ) <-> A. x ( x e. A -> ( ph -> ps ) ) )
2		impexp 263	. . . . 5 |- ( ( ( x e. A /\ ph ) -> ps ) <-> ( x e. A -> ( ph -> ps ) ) )
3	2	albii 1523	. . . 4 |- ( A. x ( ( x e. A /\ ph ) -> ps ) <-> A. x ( x e. A -> ( ph -> ps ) ) )
4	1, 3	bitr4i 187	. . 3 |- ( A. x e. A ( ph -> ps ) <-> A. x ( ( x e. A /\ ph ) -> ps ) )
5		df-reu 2535	. . 3 |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
6	4, 5	anbi12i 464	. 2 |- ( ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) <-> ( A. x ( ( x e. A /\ ph ) -> ps ) /\ E! x ( x e. A /\ ph ) ) )
7		df-ralseu 17175	. 2 |- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
8		df-alseu 17174	. 2 |- ( A.E! x ( ( x e. A /\ ph ) -> ps ) <-> ( A. x ( ( x e. A /\ ph ) -> ps ) /\ E! x ( x e. A /\ ph ) ) )
9	6, 7, 8	3bitr4i 212	1 |- ( A.E! x e. A ( ph -> ps ) <-> A.E! x ( ( x e. A /\ ph ) -> ps ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   E!weu 2086   e. wcel 2209   A.wral 2528   E!wreu 2530   A.E!walseu 17172   A.E!wralseu 17173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533  df-reu 2535  df-alseu 17174  df-ralseu 17175

This theorem is used by: (None)