Description: Similar to Theorem 7.2 of TakeutiZaring p. 35, except that the Axiom of Regularity is not required due to the antecedent _E Fr A . (Contributed by NM, 4-May-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tz7.2 | |- ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trss | |- ( Tr A -> ( B e. A -> B C_ A ) ) |
|
| 2 | efrirr | |- ( _E Fr A -> -. A e. A ) |
|
| 3 | eleq1 | |- ( B = A -> ( B e. A <-> A e. A ) ) |
|
| 4 | 3 | notbid | |- ( B = A -> ( -. B e. A <-> -. A e. A ) ) |
| 5 | 2 4 | syl5ibrcom | |- ( _E Fr A -> ( B = A -> -. B e. A ) ) |
| 6 | 5 | necon2ad | |- ( _E Fr A -> ( B e. A -> B =/= A ) ) |
| 7 | 1 6 | anim12ii | |- ( ( Tr A /\ _E Fr A ) -> ( B e. A -> ( B C_ A /\ B =/= A ) ) ) |
| 8 | 7 | 3impia | |- ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) ) |