This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ref

Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010)

Ref Expression
Assertion df-ref ⊢ Ref = x y | ⋃ y = ⋃ x ∧ ∀ z ∈ x ∃ w ∈ y z ⊆ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cref class Ref
1 vx setvar x
2 vy setvar y
3 2 cv setvar y
4 3 cuni class ⋃ y
5 1 cv setvar x
6 5 cuni class ⋃ x
7 4 6 wceq wff ⋃ y = ⋃ x
8 vz setvar z
9 vw setvar w
10 8 cv setvar z
11 9 cv setvar w
12 10 11 wss wff z ⊆ w
13 12 9 3 wrex wff ∃ w ∈ y z ⊆ w
14 13 8 5 wral wff ∀ z ∈ x ∃ w ∈ y z ⊆ w
15 7 14 wa wff ⋃ y = ⋃ x ∧ ∀ z ∈ x ∃ w ∈ y z ⊆ w
16 15 1 2 copab class x y | ⋃ y = ⋃ x ∧ ∀ z ∈ x ∃ w ∈ y z ⊆ w
17 0 16 wceq wff Ref = x y | ⋃ y = ⋃ x ∧ ∀ z ∈ x ∃ w ∈ y z ⊆ w