Description: Proof illustrating the comment of aev2 . (Contributed by BJ, 30-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | aevdemo | |- ( A. x x = y -> ( ( E. a A. b c = d \/ E. e f = g ) /\ A. h ( i = j -> k = l ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aev | |- ( A. x x = y -> A. e f = g ) |
|
| 2 | 1 | 19.2d | |- ( A. x x = y -> E. e f = g ) |
| 3 | 2 | olcd | |- ( A. x x = y -> ( E. a A. b c = d \/ E. e f = g ) ) |
| 4 | aev | |- ( A. x x = y -> A. m m = n ) |
|
| 5 | aeveq | |- ( A. m m = n -> k = l ) |
|
| 6 | 5 | a1d | |- ( A. m m = n -> ( i = j -> k = l ) ) |
| 7 | 6 | alrimiv | |- ( A. m m = n -> A. h ( i = j -> k = l ) ) |
| 8 | 4 7 | syl | |- ( A. x x = y -> A. h ( i = j -> k = l ) ) |
| 9 | 3 8 | jca | |- ( A. x x = y -> ( ( E. a A. b c = d \/ E. e f = g ) /\ A. h ( i = j -> k = l ) ) ) |