Theorem exanres3

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

	Ref	Expression
Assertion	exanres3	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝐵 ∈ [ 𝑢 ] 𝑅 ∧ 𝐶 ∈ [ 𝑢 ] 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elecALTV	⊢ ( ( 𝑢 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐵 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝐵 ) )
2	1	el2v1	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝐵 ) )
3		elecALTV	⊢ ( ( 𝑢 ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( 𝐶 ∈ [ 𝑢 ] 𝑆 ↔ 𝑢 𝑆 𝐶 ) )
4	3	el2v1	⊢ ( 𝐶 ∈ 𝑊 → ( 𝐶 ∈ [ 𝑢 ] 𝑆 ↔ 𝑢 𝑆 𝐶 ) )
5	2 4	bi2anan9	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝐵 ∈ [ 𝑢 ] 𝑅 ∧ 𝐶 ∈ [ 𝑢 ] 𝑆 ) ↔ ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ) )
6	5	rexbidv	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝐵 ∈ [ 𝑢 ] 𝑅 ∧ 𝐶 ∈ [ 𝑢 ] 𝑆 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝐵 ∧ 𝑢 𝑆 𝐶 ) ) )