Theorem fipjust 36181

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

Assertion

Ref	Expression
fipjust	|- ( A. u e. A A. v e. A ( u i^i v ) e. A <-> A. x e. A A. y e. A ( x i^i y ) e. A )

Distinct variable group:   v, u, x, y, A

Proof of Theorem fipjust

Step	Hyp	Ref	Expression
1		ineq1 3629	. . 3 |- ( u = x -> ( u i^i v ) = ( x i^i v ) )
2	1	eleq1d 2515	. 2 |- ( u = x -> ( ( u i^i v ) e. A <-> ( x i^i v ) e. A ) )
3		ineq2 3630	. . 3 |- ( v = y -> ( x i^i v ) = ( x i^i y ) )
4	3	eleq1d 2515	. 2 |- ( v = y -> ( ( x i^i v ) e. A <-> ( x i^i y ) e. A ) )
5	2, 4	cbvral2v 3029	1 |- ( A. u e. A A. v e. A ( u i^i v ) e. A <-> A. x e. A A. y e. A ( x i^i y ) e. A )

Syntax hints:   <-> wb 188   e. wcel 1889   A.wral 2739   i^i cin 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-v 3049  df-in 3413

This theorem is referenced by: (None)