Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-disoa Structured version   Visualization version   Unicode version

Definition df-disoa 34597
 Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)
Assertion
Ref Expression
df-disoa
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-disoa
StepHypRef Expression
1 cdia 34596 . 2
2 vk . . 3
3 cvv 3045 . . 3
4 vw . . . 4
52cv 1443 . . . . 5
6 clh 33549 . . . . 5
75, 6cfv 5582 . . . 4
8 vx . . . . 5
9 vy . . . . . . . 8
109cv 1443 . . . . . . 7
114cv 1443 . . . . . . 7
12 cple 15197 . . . . . . . 8
135, 12cfv 5582 . . . . . . 7
1410, 11, 13wbr 4402 . . . . . 6
15 cbs 15121 . . . . . . 7
165, 15cfv 5582 . . . . . 6
1714, 9, 16crab 2741 . . . . 5
18 vf . . . . . . . . 9
1918cv 1443 . . . . . . . 8
20 ctrl 33724 . . . . . . . . . 10
215, 20cfv 5582 . . . . . . . . 9
2211, 21cfv 5582 . . . . . . . 8
2319, 22cfv 5582 . . . . . . 7
248cv 1443 . . . . . . 7
2523, 24, 13wbr 4402 . . . . . 6
26 cltrn 33666 . . . . . . . 8
275, 26cfv 5582 . . . . . . 7
2811, 27cfv 5582 . . . . . 6
2925, 18, 28crab 2741 . . . . 5
308, 17, 29cmpt 4461 . . . 4
314, 7, 30cmpt 4461 . . 3
322, 3, 31cmpt 4461 . 2
331, 32wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  diaffval  34598
 Copyright terms: Public domain W3C validator