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