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∈AB∈uR∧C∈uS↔∃u∈AuRB∧uSC

Proof

Step Hyp Ref Expression
1 elecALTV ⊢u∈V∧B∈V→B∈uR↔uRB
2 1 el2v1 ⊢B∈V→B∈uR↔uRB
3 elecALTV ⊢u∈V∧C∈W→C∈uS↔uSC
4 3 el2v1 ⊢C∈W→C∈uS↔uSC
5 2 4 bi2anan9 ⊢B∈V∧C∈W→B∈uR∧C∈uS↔uRB∧uSC
6 5 rexbidv ⊢B∈V∧C∈W→∃u∈AB∈uR∧C∈uS↔∃u∈AuRB∧uSC