Metamath Proof Explorer

Theorem brtxpsd3

Description: A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014)

Ref Expression
Hypotheses brtxpsd2.1 ⊢ A ∈ V
brtxpsd2.2 ⊢ B ∈ V
brtxpsd2.3 ⊢ R = C ∖ ran ⁡ V ⊗ E ∆ S ⊗ V
brtxpsd2.4 ⊢ A C B
brtxpsd3.5 ⊢ x ∈ X ↔ x S A
Assertion brtxpsd3 ⊢ A R B ↔ B = X

Proof

Step Hyp Ref Expression
1 brtxpsd2.1 ⊢ A ∈ V
2 brtxpsd2.2 ⊢ B ∈ V
3 brtxpsd2.3 ⊢ R = C ∖ ran ⁡ V ⊗ E ∆ S ⊗ V
4 brtxpsd2.4 ⊢ A C B
5 brtxpsd3.5 ⊢ x ∈ X ↔ x S A
6 5 bibi2i ⊢ x ∈ B ↔ x ∈ X ↔ x ∈ B ↔ x S A
7 6 albii ⊢ ∀ x x ∈ B ↔ x ∈ X ↔ ∀ x x ∈ B ↔ x S A
8 dfcleq ⊢ B = X ↔ ∀ x x ∈ B ↔ x ∈ X
9 1 2 3 4 brtxpsd2 ⊢ A R B ↔ ∀ x x ∈ B ↔ x S A
10 7 8 9 3bitr4ri ⊢ A R B ↔ B = X