Metamath Proof Explorer

Theorem exanres3

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

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

Proof

Step Hyp Ref Expression
1 elecALTV ⊢ u ∈ V ∧ B ∈ V → B ∈ u R ↔ u R B
2 1 el2v1 ⊢ B ∈ V → B ∈ u R ↔ u R B
3 elecALTV ⊢ u ∈ V ∧ C ∈ W → C ∈ u S ↔ u S C
4 3 el2v1 ⊢ C ∈ W → C ∈ u S ↔ u S C
5 2 4 bi2anan9 ⊢ B ∈ V ∧ C ∈ W → B ∈ u R ∧ C ∈ u S ↔ u R B ∧ u S C
6 5 rexbidv ⊢ B ∈ V ∧ C ∈ W → ∃ u ∈ A B ∈ u R ∧ C ∈ u S ↔ ∃ u ∈ A u R B ∧ u S C