Description: Obsolete version of rexss as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexssOLD | |- ( A C_ B -> ( E. x e. A ph <-> E. x e. B ( x e. A /\ ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssel | |- ( A C_ B -> ( x e. A -> x e. B ) ) |
|
| 2 | 1 | pm4.71rd | |- ( A C_ B -> ( x e. A <-> ( x e. B /\ x e. A ) ) ) |
| 3 | 2 | anbi1d | |- ( A C_ B -> ( ( x e. A /\ ph ) <-> ( ( x e. B /\ x e. A ) /\ ph ) ) ) |
| 4 | anass | |- ( ( ( x e. B /\ x e. A ) /\ ph ) <-> ( x e. B /\ ( x e. A /\ ph ) ) ) |
|
| 5 | 3 4 | bitrdi | |- ( A C_ B -> ( ( x e. A /\ ph ) <-> ( x e. B /\ ( x e. A /\ ph ) ) ) ) |
| 6 | 5 | rexbidv2 | |- ( A C_ B -> ( E. x e. A ph <-> E. x e. B ( x e. A /\ ph ) ) ) |