Theorem dfralseu2 17286

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 17252. (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 17285	. 2 |- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
8		df-alseu 17284	. 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 17282   A.E!wralseu 17283

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 17284  df-ralseu 17285

This theorem is used by: (None)