Theorem exan3

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

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

Proof

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