Metamath Proof Explorer


Theorem brabgaf

Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013) (Revised by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses brabgaf.0 x ψ
brabgaf.1 x = A y = B φ ψ
brabgaf.2 R = x y | φ
Assertion brabgaf A V B W A R B ψ

Proof

Step Hyp Ref Expression
1 brabgaf.0 x ψ
2 brabgaf.1 x = A y = B φ ψ
3 brabgaf.2 R = x y | φ
4 df-br A R B A B R
5 3 eleq2i A B R A B x y | φ
6 4 5 bitri A R B A B x y | φ
7 elopab A B x y | φ x y A B = x y φ
8 elisset A V x x = A
9 elisset B W y y = B
10 exdistrv x y x = A y = B x x = A y y = B
11 nfe1 x x y A B = x y φ
12 11 1 nfbi x x y A B = x y φ ψ
13 nfe1 y y A B = x y φ
14 13 nfex y x y A B = x y φ
15 nfv y ψ
16 14 15 nfbi y x y A B = x y φ ψ
17 opeq12 x = A y = B x y = A B
18 copsexgw A B = x y φ x y A B = x y φ
19 18 eqcoms x y = A B φ x y A B = x y φ
20 17 19 syl x = A y = B φ x y A B = x y φ
21 20 2 bitr3d x = A y = B x y A B = x y φ ψ
22 16 21 exlimi y x = A y = B x y A B = x y φ ψ
23 12 22 exlimi x y x = A y = B x y A B = x y φ ψ
24 10 23 sylbir x x = A y y = B x y A B = x y φ ψ
25 8 9 24 syl2an A V B W x y A B = x y φ ψ
26 7 25 syl5bb A V B W A B x y | φ ψ
27 6 26 syl5bb A V B W A R B ψ