MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ref Structured version   Visualization version   GIF version

Definition df-ref 22041
Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)
Assertion
Ref Expression
df-ref Ref = {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
Distinct variable group:   𝑥,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-ref
StepHypRef Expression
1 cref 22038 . 2 class Ref
2 vy . . . . . . 7 setvar 𝑦
32cv 1527 . . . . . 6 class 𝑦
43cuni 4830 . . . . 5 class 𝑦
5 vx . . . . . . 7 setvar 𝑥
65cv 1527 . . . . . 6 class 𝑥
76cuni 4830 . . . . 5 class 𝑥
84, 7wceq 1528 . . . 4 wff 𝑦 = 𝑥
9 vz . . . . . . . 8 setvar 𝑧
109cv 1527 . . . . . . 7 class 𝑧
11 vw . . . . . . . 8 setvar 𝑤
1211cv 1527 . . . . . . 7 class 𝑤
1310, 12wss 3933 . . . . . 6 wff 𝑧𝑤
1413, 11, 3wrex 3136 . . . . 5 wff 𝑤𝑦 𝑧𝑤
1514, 9, 6wral 3135 . . . 4 wff 𝑧𝑥𝑤𝑦 𝑧𝑤
168, 15wa 396 . . 3 wff ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)
1716, 5, 2copab 5119 . 2 class {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
181, 17wceq 1528 1 wff Ref = {⟨𝑥, 𝑦⟩ ∣ ( 𝑦 = 𝑥 ∧ ∀𝑧𝑥𝑤𝑦 𝑧𝑤)}
Colors of variables: wff setvar class
This definition is referenced by:  refrel  22044  isref  22045
  Copyright terms: Public domain W3C validator