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 ⊢¬Aran⁡V⊗E∆R⊗VB↔∀xx∈B↔xRA

Proof

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