Metamath Proof Explorer

Theorem exan3

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

Ref Expression
Assertion exan3 ⊢ A ∈ V ∧ B ∈ W → ∃ u A ∈ u R ∧ B ∈ u R ↔ ∃ u u R A ∧ u R B

Proof

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