Theorem inex3

Description: Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019)

	Ref	Expression
Assertion	inex3	$$⊢\left(A\in V\vee B\in W\right)\to A\cap B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		inex1g	$$⊢A\in V\to A\cap B\in \mathrm{V}$$
2		inex2g	$$⊢B\in W\to A\cap B\in \mathrm{V}$$
3	1 2	jaoi	$$⊢\left(A\in V\vee B\in W\right)\to A\cap B\in \mathrm{V}$$