Description: Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of Enderton p. 146. (Contributed by NM, 24-Apr-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | domeng | |- ( B e. C -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | breq2 | |- ( y = B -> ( A ~<_ y <-> A ~<_ B ) ) |
|
| 2 | sseq2 | |- ( y = B -> ( x C_ y <-> x C_ B ) ) |
|
| 3 | 2 | anbi2d | |- ( y = B -> ( ( A ~~ x /\ x C_ y ) <-> ( A ~~ x /\ x C_ B ) ) ) |
| 4 | 3 | exbidv | |- ( y = B -> ( E. x ( A ~~ x /\ x C_ y ) <-> E. x ( A ~~ x /\ x C_ B ) ) ) |
| 5 | vex | |- y e. _V |
|
| 6 | 5 | domen | |- ( A ~<_ y <-> E. x ( A ~~ x /\ x C_ y ) ) |
| 7 | 1 4 6 | vtoclbg | |- ( B e. C -> ( A ~<_ B <-> E. x ( A ~~ x /\ x C_ B ) ) ) |