Metamath Proof Explorer

Theorem exanres2

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

Ref Expression
Assertion exanres2 ⊢ B ∈ V ∧ C ∈ W → ∃ u u R ↾ A B ∧ u S ↾ A C ↔ ∃ u ∈ A B ∈ u R ∧ C ∈ u S

Proof

Step Hyp Ref Expression
1 exanres ⊢ B ∈ V ∧ C ∈ W → ∃ u u R ↾ A B ∧ u S ↾ A C ↔ ∃ u ∈ A u R B ∧ u S C
2 exanres3 ⊢ B ∈ V ∧ C ∈ W → ∃ u ∈ A B ∈ u R ∧ C ∈ u S ↔ ∃ u ∈ A u R B ∧ u S C
3 1 2 bitr4d ⊢ B ∈ V ∧ C ∈ W → ∃ u u R ↾ A B ∧ u S ↾ A C ↔ ∃ u ∈ A B ∈ u R ∧ C ∈ u S