Step |
Hyp |
Ref |
Expression |
1 |
|
psseq2 |
|- ( x = A -> ( y C. x <-> y C. A ) ) |
2 |
|
breq2 |
|- ( x = A -> ( y ~~ x <-> y ~~ A ) ) |
3 |
1 2
|
anbi12d |
|- ( x = A -> ( ( y C. x /\ y ~~ x ) <-> ( y C. A /\ y ~~ A ) ) ) |
4 |
3
|
exbidv |
|- ( x = A -> ( E. y ( y C. x /\ y ~~ x ) <-> E. y ( y C. A /\ y ~~ A ) ) ) |
5 |
4
|
notbid |
|- ( x = A -> ( -. E. y ( y C. x /\ y ~~ x ) <-> -. E. y ( y C. A /\ y ~~ A ) ) ) |
6 |
|
df-fin4 |
|- Fin4 = { x | -. E. y ( y C. x /\ y ~~ x ) } |
7 |
5 6
|
elab2g |
|- ( A e. V -> ( A e. Fin4 <-> -. E. y ( y C. A /\ y ~~ A ) ) ) |