Metamath Proof Explorer

Theorem bnj1414

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1414.1 ⊢ B = pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R
Assertion bnj1414 ⊢ R FrSe A ∧ X ∈ A → trCl X A R = B

Proof

Step Hyp Ref Expression
1 bnj1414.1 ⊢ B = pred X A R ∪ ⋃ y ∈ pred X A R trCl y A R
2 eqid ⊢ pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R = pred X A R ∪ ⋃ y ∈ trCl X A R trCl y A R
3 biid ⊢ R FrSe A ∧ X ∈ A ↔ R FrSe A ∧ X ∈ A
4 biid ⊢ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B ↔ B ∈ V ∧ TrFo B A R ∧ pred X A R ⊆ B
5 1 2 3 4 bnj1408 ⊢ R FrSe A ∧ X ∈ A → trCl X A R = B