Theorem dfralseu2 17383

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 17349. (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 17382	. 2 |- ( A.E! x e. A ( ph -> ps ) <-> ( A. x e. A ( ph -> ps ) /\ E! x e. A ph ) )
8		df-alseu 17381	. 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 17379   A.E!wralseu 17380

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 17381  df-ralseu 17382

This theorem is used by: (None)