This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brtxpsd

Description: Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brtxpsd.1 ⊢ A ∈ V
brtxpsd.2 ⊢ B ∈ V
Assertion brtxpsd ⊢ ¬ A ran ⁡ V ⊗ E ∆ R ⊗ V B ↔ ∀ x x ∈ B ↔ x R A

Proof

Step Hyp Ref Expression
1 brtxpsd.1 ⊢ A ∈ V
2 brtxpsd.2 ⊢ B ∈ V
3 df-br ⊢ A ran ⁡ V ⊗ E ∆ R ⊗ V B ↔ A B ∈ ran ⁡ V ⊗ E ∆ R ⊗ V
4 opex ⊢ A B ∈ V
5 4 elrn ⊢ A B ∈ ran ⁡ V ⊗ E ∆ R ⊗ V ↔ ∃ x x V ⊗ E ∆ R ⊗ V A B
6 brsymdif ⊢ x V ⊗ E ∆ R ⊗ V A B ↔ ¬ x V ⊗ E A B ↔ x R ⊗ V A B
7 brv ⊢ x V A
8 vex ⊢ x ∈ V
9 8 1 2 brtxp ⊢ x V ⊗ E A B ↔ x V A ∧ x E B
10 7 9 mpbiran ⊢ x V ⊗ E A B ↔ x E B
11 2 epeli ⊢ x E B ↔ x ∈ B
12 10 11 bitri ⊢ x V ⊗ E A B ↔ x ∈ B
13 brv ⊢ x V B
14 8 1 2 brtxp ⊢ x R ⊗ V A B ↔ x R A ∧ x V B
15 13 14 mpbiran2 ⊢ x R ⊗ V A B ↔ x R A
16 12 15 bibi12i ⊢ x V ⊗ E A B ↔ x R ⊗ V A B ↔ x ∈ B ↔ x R A
17 6 16 xchbinx ⊢ x V ⊗ E ∆ R ⊗ V A B ↔ ¬ x ∈ B ↔ x R A
18 17 exbii ⊢ ∃ x x V ⊗ E ∆ R ⊗ V A B ↔ ∃ x ¬ x ∈ B ↔ x R A
19 5 18 bitri ⊢ A B ∈ ran ⁡ V ⊗ E ∆ R ⊗ V ↔ ∃ x ¬ x ∈ B ↔ x R A
20 exnal ⊢ ∃ x ¬ x ∈ B ↔ x R A ↔ ¬ ∀ x x ∈ B ↔ x R A
21 3 19 20 3bitrri ⊢ ¬ ∀ x x ∈ B ↔ x R A ↔ A ran ⁡ V ⊗ E ∆ R ⊗ V B
22 21 con1bii ⊢ ¬ A ran ⁡ V ⊗ E ∆ R ⊗ V B ↔ ∀ x x ∈ B ↔ x R A