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 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trss | ⊢ ( Tr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴 ) ) | |
| 2 | efrirr | ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴 ) | |
| 3 | eleq1 | ⊢ ( 𝐵 = 𝐴 → ( 𝐵 ∈ 𝐴 ↔ 𝐴 ∈ 𝐴 ) ) | |
| 4 | 3 | notbid | ⊢ ( 𝐵 = 𝐴 → ( ¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐴 ∈ 𝐴 ) ) |
| 5 | 2 4 | syl5ibrcom | ⊢ ( E Fr 𝐴 → ( 𝐵 = 𝐴 → ¬ 𝐵 ∈ 𝐴 ) ) |
| 6 | 5 | necon2ad | ⊢ ( E Fr 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ≠ 𝐴 ) ) |
| 7 | 1 6 | anim12ii | ⊢ ( ( Tr 𝐴 ∧ E Fr 𝐴 ) → ( 𝐵 ∈ 𝐴 → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) ) |
| 8 | 7 | 3impia | ⊢ ( ( Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴 ) ) |