Metamath Proof Explorer


Theorem exanres

Description: Equivalent expressions with existential quantification. (Contributed by Peter Mazsa, 2-May-2021)

Ref Expression
Assertion exanres B V C W u u R A B u S A C u A u R B u S C

Proof

Step Hyp Ref Expression
1 brres B V u R A B u A u R B
2 brres C W u S A C u A u S C
3 1 2 bi2anan9 B V C W u R A B u S A C u A u R B u A u S C
4 anandi u A u R B u S C u A u R B u A u S C
5 3 4 bitr4di B V C W u R A B u S A C u A u R B u S C
6 5 exbidv B V C W u u R A B u S A C u u A u R B u S C
7 df-rex u A u R B u S C u u A u R B u S C
8 6 7 bitr4di B V C W u u R A B u S A C u A u R B u S C