Metamath Proof Explorer


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 ( ∀ 𝑢𝐴𝑣𝐴 ( 𝑢𝑣 ) ∈ 𝐴 ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 ineq1 ( 𝑢 = 𝑥 → ( 𝑢𝑣 ) = ( 𝑥𝑣 ) )
2 1 eleq1d ( 𝑢 = 𝑥 → ( ( 𝑢𝑣 ) ∈ 𝐴 ↔ ( 𝑥𝑣 ) ∈ 𝐴 ) )
3 ineq2 ( 𝑣 = 𝑦 → ( 𝑥𝑣 ) = ( 𝑥𝑦 ) )
4 3 eleq1d ( 𝑣 = 𝑦 → ( ( 𝑥𝑣 ) ∈ 𝐴 ↔ ( 𝑥𝑦 ) ∈ 𝐴 ) )
5 2 4 cbvral2vw ( ∀ 𝑢𝐴𝑣𝐴 ( 𝑢𝑣 ) ∈ 𝐴 ↔ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )