Theorem fipjust

Description: A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020)

	Ref	Expression
Assertion	fipjust	$$⊢\forall u\in A\forall v\in Au\cap v\in A\leftrightarrow \forall x\in A\forall y\in Ax\cap y\in A$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢u=x\to u\cap v=x\cap v$$
2	1	eleq1d	$$⊢u=x\to \left(u\cap v\in A\leftrightarrow x\cap v\in A\right)$$
3		ineq2	$$⊢v=y\to x\cap v=x\cap y$$
4	3	eleq1d	$$⊢v=y\to \left(x\cap v\in A\leftrightarrow x\cap y\in A\right)$$
5	2 4	cbvral2vw	$$⊢\forall u\in A\forall v\in Au\cap v\in A\leftrightarrow \forall x\in A\forall y\in Ax\cap y\in A$$