Metamath Proof Explorer

Theorem brtxpsd2

Description: Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-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
Assertion brtxpsd2 ⊢ A R B ↔ ∀ x x ∈ B ↔ x S A

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 3 breqi ⊢ A R B ↔ A C ∖ ran ⁡ V ⊗ E ∆ S ⊗ V B
6 brdif ⊢ A C ∖ ran ⁡ V ⊗ E ∆ S ⊗ V B ↔ A C B ∧ ¬ A ran ⁡ V ⊗ E ∆ S ⊗ V B
7 5 6 bitri ⊢ A R B ↔ A C B ∧ ¬ A ran ⁡ V ⊗ E ∆ S ⊗ V B
8 4 7 mpbiran ⊢ A R B ↔ ¬ A ran ⁡ V ⊗ E ∆ S ⊗ V B
9 1 2 brtxpsd ⊢ ¬ A ran ⁡ V ⊗ E ∆ S ⊗ V B ↔ ∀ x x ∈ B ↔ x S A
10 8 9 bitri ⊢ A R B ↔ ∀ x x ∈ B ↔ x S A