Theorem dfralseu2 17138

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 17104. (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 17137	. 2 |- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
8		df-alseu 17136	. 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 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1400   E!weu 2086   e. wcel 2209   A.wral 2528   E!wreu 2530   A.E!walseu 17134   A.E!wralseu 17135

This theorem was proved from 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 theorem depends on definitions:  df-bi 117  df-ral 2533  df-reu 2535  df-alseu 17136  df-ralseu 17137

This theorem is referenced by: (None)