# Metamath Proof Explorer

## Theorem tz7.2

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 ${⊢}\left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{Fr}{A}\wedge {B}\in {A}\right)\to \left({B}\subseteq {A}\wedge {B}\ne {A}\right)$

### Proof

Step Hyp Ref Expression
1 trss ${⊢}\mathrm{Tr}{A}\to \left({B}\in {A}\to {B}\subseteq {A}\right)$
2 efrirr ${⊢}\mathrm{E}\mathrm{Fr}{A}\to ¬{A}\in {A}$
3 eleq1 ${⊢}{B}={A}\to \left({B}\in {A}↔{A}\in {A}\right)$
4 3 notbid ${⊢}{B}={A}\to \left(¬{B}\in {A}↔¬{A}\in {A}\right)$
5 2 4 syl5ibrcom ${⊢}\mathrm{E}\mathrm{Fr}{A}\to \left({B}={A}\to ¬{B}\in {A}\right)$
6 5 necon2ad ${⊢}\mathrm{E}\mathrm{Fr}{A}\to \left({B}\in {A}\to {B}\ne {A}\right)$
7 1 6 anim12ii ${⊢}\left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{Fr}{A}\right)\to \left({B}\in {A}\to \left({B}\subseteq {A}\wedge {B}\ne {A}\right)\right)$
8 7 3impia ${⊢}\left(\mathrm{Tr}{A}\wedge \mathrm{E}\mathrm{Fr}{A}\wedge {B}\in {A}\right)\to \left({B}\subseteq {A}\wedge {B}\ne {A}\right)$